{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE UndecidableInstances #-}

-- | Methods to match patterns in 'EGraph's (aka e-matching)
module Overeasy.Matching
  ( Pat
  , patVars
  , PatGroup
  , Subst
  , substVars
  , VarId (..)
  , PatGraphC
  , PatGraph (..)
  , patGraph
  , singlePatGraph
  , Match (..)
  , MatchPat (..)
  , MatchF (..)
  , MatchPatF (..)
  , matchVars
  , matchClasses
  , MatchSubst (..)
  , SolGraphC
  , SolGraph (..)
  , solGraph
  , SolStream
  , SolveC
  , solve
  , match
  ) where

import Control.Applicative (Alternative (..))
import Control.DeepSeq (NFData)
import Control.Monad (void)
import Control.Monad.Identity (Identity (..))
import Control.Monad.Reader (asks)
import Control.Monad.State.Strict (MonadState (..), State, evalState, execState, gets, modify', runState)
import Data.Bifunctor (bimap)
import Data.Coerce (Coercible)
import Data.Foldable (fold, foldMap', foldl', for_, toList)
import Data.Functor.Foldable (Base, Corecursive (..), Recursive (..), cata)
import Data.Hashable (Hashable)
import Data.HashMap.Strict (HashMap)
import qualified Data.HashMap.Strict as HashMap
import Data.HashSet (HashSet)
import qualified Data.HashSet as HashSet
import IntLike.Map (IntLikeMap)
import qualified IntLike.Map as ILM
import IntLike.Set (IntLikeSet)
import qualified IntLike.Set as ILS
import Overeasy.Assoc (Assoc, assocBwd, assocEquiv, assocFootprint, assocFwd, assocInsertInc, assocLookupByValue,
                       assocNew)
import Overeasy.EGraph (EClassId (..), EGraph (egHashCons), ENodeId (..), eciNodes, egClassMap, egNodeAssoc)
import Overeasy.EquivFind (efLookupRoot)
import Overeasy.Source (Source, sourceAddInc, sourceNew)
import Overeasy.Streams (Stream, chooseWith, streamAll)
import Unfree (Free, FreeF (..))

-- | A pattern is exactly the free monad over the expression functor
-- It has spots for var names ('FreePure') and spots for structural
-- pieces ('FreeEmbed')
type Pat = Free

-- | The base functor of 'Pat'.
type PatF = FreeF

-- | The set of vars for a pattern.
patVars :: (Foldable f, Eq v, Hashable v) => Pat f v -> HashSet v
patVars :: forall (f :: * -> *) v.
(Foldable f, Eq v, Hashable v) =>
Pat f v -> HashSet v
patVars = forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap' forall a. Hashable a => a -> HashSet a
HashSet.singleton

-- | A pattern group is some container with patterns inside.
-- This container might be 'Identity' for one pattern, or a list or
-- map for many patterns.
type PatGroup g f v = g (Pat f v)

-- | A substitution.
type Subst c v = HashMap v c

-- | The set of vars for a substitution.
substVars :: Subst a v -> HashSet v
substVars :: forall a v. Subst a v -> HashSet v
substVars = forall k a. HashMap k a -> HashSet k
HashMap.keysSet

-- | A match is a pattern annotated with classes (or other data).
data Match c f v = Match
  { forall c (f :: * -> *) v. Match c f v -> c
matchAnno :: !c
  , forall c (f :: * -> *) v. Match c f v -> MatchPat c f v
matchPat :: !(MatchPat c f v)
  } deriving stock (forall a b. a -> Match c f b -> Match c f a
forall a b. (a -> b) -> Match c f a -> Match c f b
forall c (f :: * -> *) a b.
Functor f =>
a -> Match c f b -> Match c f a
forall c (f :: * -> *) a b.
Functor f =>
(a -> b) -> Match c f a -> Match c f b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: forall a b. a -> Match c f b -> Match c f a
$c<$ :: forall c (f :: * -> *) a b.
Functor f =>
a -> Match c f b -> Match c f a
fmap :: forall a b. (a -> b) -> Match c f a -> Match c f b
$cfmap :: forall c (f :: * -> *) a b.
Functor f =>
(a -> b) -> Match c f a -> Match c f b
Functor, forall a. Match c f a -> Bool
forall m a. Monoid m => (a -> m) -> Match c f a -> m
forall a b. (a -> b -> b) -> b -> Match c f a -> b
forall c (f :: * -> *) a.
(Foldable f, Eq a) =>
a -> Match c f a -> Bool
forall c (f :: * -> *) a. (Foldable f, Num a) => Match c f a -> a
forall c (f :: * -> *) a. (Foldable f, Ord a) => Match c f a -> a
forall c (f :: * -> *) m.
(Foldable f, Monoid m) =>
Match c f m -> m
forall c (f :: * -> *) a. Foldable f => Match c f a -> Bool
forall c (f :: * -> *) a. Foldable f => Match c f a -> Int
forall c (f :: * -> *) a. Foldable f => Match c f a -> [a]
forall c (f :: * -> *) a.
Foldable f =>
(a -> a -> a) -> Match c f a -> a
forall c (f :: * -> *) m a.
(Foldable f, Monoid m) =>
(a -> m) -> Match c f a -> m
forall c (f :: * -> *) b a.
Foldable f =>
(b -> a -> b) -> b -> Match c f a -> b
forall c (f :: * -> *) a b.
Foldable f =>
(a -> b -> b) -> b -> Match c f a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
product :: forall a. Num a => Match c f a -> a
$cproduct :: forall c (f :: * -> *) a. (Foldable f, Num a) => Match c f a -> a
sum :: forall a. Num a => Match c f a -> a
$csum :: forall c (f :: * -> *) a. (Foldable f, Num a) => Match c f a -> a
minimum :: forall a. Ord a => Match c f a -> a
$cminimum :: forall c (f :: * -> *) a. (Foldable f, Ord a) => Match c f a -> a
maximum :: forall a. Ord a => Match c f a -> a
$cmaximum :: forall c (f :: * -> *) a. (Foldable f, Ord a) => Match c f a -> a
elem :: forall a. Eq a => a -> Match c f a -> Bool
$celem :: forall c (f :: * -> *) a.
(Foldable f, Eq a) =>
a -> Match c f a -> Bool
length :: forall a. Match c f a -> Int
$clength :: forall c (f :: * -> *) a. Foldable f => Match c f a -> Int
null :: forall a. Match c f a -> Bool
$cnull :: forall c (f :: * -> *) a. Foldable f => Match c f a -> Bool
toList :: forall a. Match c f a -> [a]
$ctoList :: forall c (f :: * -> *) a. Foldable f => Match c f a -> [a]
foldl1 :: forall a. (a -> a -> a) -> Match c f a -> a
$cfoldl1 :: forall c (f :: * -> *) a.
Foldable f =>
(a -> a -> a) -> Match c f a -> a
foldr1 :: forall a. (a -> a -> a) -> Match c f a -> a
$cfoldr1 :: forall c (f :: * -> *) a.
Foldable f =>
(a -> a -> a) -> Match c f a -> a
foldl' :: forall b a. (b -> a -> b) -> b -> Match c f a -> b
$cfoldl' :: forall c (f :: * -> *) b a.
Foldable f =>
(b -> a -> b) -> b -> Match c f a -> b
foldl :: forall b a. (b -> a -> b) -> b -> Match c f a -> b
$cfoldl :: forall c (f :: * -> *) b a.
Foldable f =>
(b -> a -> b) -> b -> Match c f a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> Match c f a -> b
$cfoldr' :: forall c (f :: * -> *) a b.
Foldable f =>
(a -> b -> b) -> b -> Match c f a -> b
foldr :: forall a b. (a -> b -> b) -> b -> Match c f a -> b
$cfoldr :: forall c (f :: * -> *) a b.
Foldable f =>
(a -> b -> b) -> b -> Match c f a -> b
foldMap' :: forall m a. Monoid m => (a -> m) -> Match c f a -> m
$cfoldMap' :: forall c (f :: * -> *) m a.
(Foldable f, Monoid m) =>
(a -> m) -> Match c f a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> Match c f a -> m
$cfoldMap :: forall c (f :: * -> *) m a.
(Foldable f, Monoid m) =>
(a -> m) -> Match c f a -> m
fold :: forall m. Monoid m => Match c f m -> m
$cfold :: forall c (f :: * -> *) m.
(Foldable f, Monoid m) =>
Match c f m -> m
Foldable, forall {c} {f :: * -> *}. Traversable f => Functor (Match c f)
forall {c} {f :: * -> *}. Traversable f => Foldable (Match c f)
forall c (f :: * -> *) (m :: * -> *) a.
(Traversable f, Monad m) =>
Match c f (m a) -> m (Match c f a)
forall c (f :: * -> *) (f :: * -> *) a.
(Traversable f, Applicative f) =>
Match c f (f a) -> f (Match c f a)
forall c (f :: * -> *) (m :: * -> *) a b.
(Traversable f, Monad m) =>
(a -> m b) -> Match c f a -> m (Match c f b)
forall c (f :: * -> *) (f :: * -> *) a b.
(Traversable f, Applicative f) =>
(a -> f b) -> Match c f a -> f (Match c f b)
forall (t :: * -> *).
Functor t
-> Foldable t
-> (forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Match c f a -> f (Match c f b)
sequence :: forall (m :: * -> *) a.
Monad m =>
Match c f (m a) -> m (Match c f a)
$csequence :: forall c (f :: * -> *) (m :: * -> *) a.
(Traversable f, Monad m) =>
Match c f (m a) -> m (Match c f a)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Match c f a -> m (Match c f b)
$cmapM :: forall c (f :: * -> *) (m :: * -> *) a b.
(Traversable f, Monad m) =>
(a -> m b) -> Match c f a -> m (Match c f b)
sequenceA :: forall (f :: * -> *) a.
Applicative f =>
Match c f (f a) -> f (Match c f a)
$csequenceA :: forall c (f :: * -> *) (f :: * -> *) a.
(Traversable f, Applicative f) =>
Match c f (f a) -> f (Match c f a)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Match c f a -> f (Match c f b)
$ctraverse :: forall c (f :: * -> *) (f :: * -> *) a b.
(Traversable f, Applicative f) =>
(a -> f b) -> Match c f a -> f (Match c f b)
Traversable)

deriving stock instance (Eq c, Eq v, Eq (f (Match c f v))) => Eq (Match c f v)
deriving stock instance (Show c, Show v, Show (f (Match c f v))) => Show (Match c f v)

-- | Tie the knot - the inner layer of a match.
data MatchPat c f v =
    MatchPatPure !v
  | MatchPatEmbed !(f (Match c f v))
  deriving stock (forall a b. a -> MatchPat c f b -> MatchPat c f a
forall a b. (a -> b) -> MatchPat c f a -> MatchPat c f b
forall c (f :: * -> *) a b.
Functor f =>
a -> MatchPat c f b -> MatchPat c f a
forall c (f :: * -> *) a b.
Functor f =>
(a -> b) -> MatchPat c f a -> MatchPat c f b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: forall a b. a -> MatchPat c f b -> MatchPat c f a
$c<$ :: forall c (f :: * -> *) a b.
Functor f =>
a -> MatchPat c f b -> MatchPat c f a
fmap :: forall a b. (a -> b) -> MatchPat c f a -> MatchPat c f b
$cfmap :: forall c (f :: * -> *) a b.
Functor f =>
(a -> b) -> MatchPat c f a -> MatchPat c f b
Functor, forall a. MatchPat c f a -> Bool
forall m a. Monoid m => (a -> m) -> MatchPat c f a -> m
forall a b. (a -> b -> b) -> b -> MatchPat c f a -> b
forall c (f :: * -> *) a.
(Foldable f, Eq a) =>
a -> MatchPat c f a -> Bool
forall c (f :: * -> *) a.
(Foldable f, Num a) =>
MatchPat c f a -> a
forall c (f :: * -> *) a.
(Foldable f, Ord a) =>
MatchPat c f a -> a
forall c (f :: * -> *) m.
(Foldable f, Monoid m) =>
MatchPat c f m -> m
forall c (f :: * -> *) a. Foldable f => MatchPat c f a -> Bool
forall c (f :: * -> *) a. Foldable f => MatchPat c f a -> Int
forall c (f :: * -> *) a. Foldable f => MatchPat c f a -> [a]
forall c (f :: * -> *) a.
Foldable f =>
(a -> a -> a) -> MatchPat c f a -> a
forall c (f :: * -> *) m a.
(Foldable f, Monoid m) =>
(a -> m) -> MatchPat c f a -> m
forall c (f :: * -> *) b a.
Foldable f =>
(b -> a -> b) -> b -> MatchPat c f a -> b
forall c (f :: * -> *) a b.
Foldable f =>
(a -> b -> b) -> b -> MatchPat c f a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
product :: forall a. Num a => MatchPat c f a -> a
$cproduct :: forall c (f :: * -> *) a.
(Foldable f, Num a) =>
MatchPat c f a -> a
sum :: forall a. Num a => MatchPat c f a -> a
$csum :: forall c (f :: * -> *) a.
(Foldable f, Num a) =>
MatchPat c f a -> a
minimum :: forall a. Ord a => MatchPat c f a -> a
$cminimum :: forall c (f :: * -> *) a.
(Foldable f, Ord a) =>
MatchPat c f a -> a
maximum :: forall a. Ord a => MatchPat c f a -> a
$cmaximum :: forall c (f :: * -> *) a.
(Foldable f, Ord a) =>
MatchPat c f a -> a
elem :: forall a. Eq a => a -> MatchPat c f a -> Bool
$celem :: forall c (f :: * -> *) a.
(Foldable f, Eq a) =>
a -> MatchPat c f a -> Bool
length :: forall a. MatchPat c f a -> Int
$clength :: forall c (f :: * -> *) a. Foldable f => MatchPat c f a -> Int
null :: forall a. MatchPat c f a -> Bool
$cnull :: forall c (f :: * -> *) a. Foldable f => MatchPat c f a -> Bool
toList :: forall a. MatchPat c f a -> [a]
$ctoList :: forall c (f :: * -> *) a. Foldable f => MatchPat c f a -> [a]
foldl1 :: forall a. (a -> a -> a) -> MatchPat c f a -> a
$cfoldl1 :: forall c (f :: * -> *) a.
Foldable f =>
(a -> a -> a) -> MatchPat c f a -> a
foldr1 :: forall a. (a -> a -> a) -> MatchPat c f a -> a
$cfoldr1 :: forall c (f :: * -> *) a.
Foldable f =>
(a -> a -> a) -> MatchPat c f a -> a
foldl' :: forall b a. (b -> a -> b) -> b -> MatchPat c f a -> b
$cfoldl' :: forall c (f :: * -> *) b a.
Foldable f =>
(b -> a -> b) -> b -> MatchPat c f a -> b
foldl :: forall b a. (b -> a -> b) -> b -> MatchPat c f a -> b
$cfoldl :: forall c (f :: * -> *) b a.
Foldable f =>
(b -> a -> b) -> b -> MatchPat c f a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> MatchPat c f a -> b
$cfoldr' :: forall c (f :: * -> *) a b.
Foldable f =>
(a -> b -> b) -> b -> MatchPat c f a -> b
foldr :: forall a b. (a -> b -> b) -> b -> MatchPat c f a -> b
$cfoldr :: forall c (f :: * -> *) a b.
Foldable f =>
(a -> b -> b) -> b -> MatchPat c f a -> b
foldMap' :: forall m a. Monoid m => (a -> m) -> MatchPat c f a -> m
$cfoldMap' :: forall c (f :: * -> *) m a.
(Foldable f, Monoid m) =>
(a -> m) -> MatchPat c f a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> MatchPat c f a -> m
$cfoldMap :: forall c (f :: * -> *) m a.
(Foldable f, Monoid m) =>
(a -> m) -> MatchPat c f a -> m
fold :: forall m. Monoid m => MatchPat c f m -> m
$cfold :: forall c (f :: * -> *) m.
(Foldable f, Monoid m) =>
MatchPat c f m -> m
Foldable, forall {c} {f :: * -> *}. Traversable f => Functor (MatchPat c f)
forall {c} {f :: * -> *}. Traversable f => Foldable (MatchPat c f)
forall c (f :: * -> *) (m :: * -> *) a.
(Traversable f, Monad m) =>
MatchPat c f (m a) -> m (MatchPat c f a)
forall c (f :: * -> *) (f :: * -> *) a.
(Traversable f, Applicative f) =>
MatchPat c f (f a) -> f (MatchPat c f a)
forall c (f :: * -> *) (m :: * -> *) a b.
(Traversable f, Monad m) =>
(a -> m b) -> MatchPat c f a -> m (MatchPat c f b)
forall c (f :: * -> *) (f :: * -> *) a b.
(Traversable f, Applicative f) =>
(a -> f b) -> MatchPat c f a -> f (MatchPat c f b)
forall (t :: * -> *).
Functor t
-> Foldable t
-> (forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> MatchPat c f a -> f (MatchPat c f b)
sequence :: forall (m :: * -> *) a.
Monad m =>
MatchPat c f (m a) -> m (MatchPat c f a)
$csequence :: forall c (f :: * -> *) (m :: * -> *) a.
(Traversable f, Monad m) =>
MatchPat c f (m a) -> m (MatchPat c f a)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> MatchPat c f a -> m (MatchPat c f b)
$cmapM :: forall c (f :: * -> *) (m :: * -> *) a b.
(Traversable f, Monad m) =>
(a -> m b) -> MatchPat c f a -> m (MatchPat c f b)
sequenceA :: forall (f :: * -> *) a.
Applicative f =>
MatchPat c f (f a) -> f (MatchPat c f a)
$csequenceA :: forall c (f :: * -> *) (f :: * -> *) a.
(Traversable f, Applicative f) =>
MatchPat c f (f a) -> f (MatchPat c f a)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> MatchPat c f a -> f (MatchPat c f b)
$ctraverse :: forall c (f :: * -> *) (f :: * -> *) a b.
(Traversable f, Applicative f) =>
(a -> f b) -> MatchPat c f a -> f (MatchPat c f b)
Traversable)

deriving stock instance (Eq v, Eq (f (Match c f v))) => Eq (MatchPat c f v)
deriving stock instance (Show v, Show (f (Match c f v))) => Show (MatchPat c f v)

-- | The base functor of 'Match'
data MatchF c f v r = MatchF
  { forall c (f :: * -> *) v r. MatchF c f v r -> c
matchClassF :: !c
  , forall c (f :: * -> *) v r. MatchF c f v r -> MatchPatF f v r
matchPatF :: !(MatchPatF f v r)
  } deriving stock (forall a b. a -> MatchF c f v b -> MatchF c f v a
forall a b. (a -> b) -> MatchF c f v a -> MatchF c f v b
forall c (f :: * -> *) v a b.
Functor f =>
a -> MatchF c f v b -> MatchF c f v a
forall c (f :: * -> *) v a b.
Functor f =>
(a -> b) -> MatchF c f v a -> MatchF c f v b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: forall a b. a -> MatchF c f v b -> MatchF c f v a
$c<$ :: forall c (f :: * -> *) v a b.
Functor f =>
a -> MatchF c f v b -> MatchF c f v a
fmap :: forall a b. (a -> b) -> MatchF c f v a -> MatchF c f v b
$cfmap :: forall c (f :: * -> *) v a b.
Functor f =>
(a -> b) -> MatchF c f v a -> MatchF c f v b
Functor, forall a. MatchF c f v a -> Bool
forall m a. Monoid m => (a -> m) -> MatchF c f v a -> m
forall a b. (a -> b -> b) -> b -> MatchF c f v a -> b
forall c (f :: * -> *) v a.
(Foldable f, Eq a) =>
a -> MatchF c f v a -> Bool
forall c (f :: * -> *) v a.
(Foldable f, Num a) =>
MatchF c f v a -> a
forall c (f :: * -> *) v a.
(Foldable f, Ord a) =>
MatchF c f v a -> a
forall c (f :: * -> *) v m.
(Foldable f, Monoid m) =>
MatchF c f v m -> m
forall c (f :: * -> *) v a. Foldable f => MatchF c f v a -> Bool
forall c (f :: * -> *) v a. Foldable f => MatchF c f v a -> Int
forall c (f :: * -> *) v a. Foldable f => MatchF c f v a -> [a]
forall c (f :: * -> *) v a.
Foldable f =>
(a -> a -> a) -> MatchF c f v a -> a
forall c (f :: * -> *) v m a.
(Foldable f, Monoid m) =>
(a -> m) -> MatchF c f v a -> m
forall c (f :: * -> *) v b a.
Foldable f =>
(b -> a -> b) -> b -> MatchF c f v a -> b
forall c (f :: * -> *) v a b.
Foldable f =>
(a -> b -> b) -> b -> MatchF c f v a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
product :: forall a. Num a => MatchF c f v a -> a
$cproduct :: forall c (f :: * -> *) v a.
(Foldable f, Num a) =>
MatchF c f v a -> a
sum :: forall a. Num a => MatchF c f v a -> a
$csum :: forall c (f :: * -> *) v a.
(Foldable f, Num a) =>
MatchF c f v a -> a
minimum :: forall a. Ord a => MatchF c f v a -> a
$cminimum :: forall c (f :: * -> *) v a.
(Foldable f, Ord a) =>
MatchF c f v a -> a
maximum :: forall a. Ord a => MatchF c f v a -> a
$cmaximum :: forall c (f :: * -> *) v a.
(Foldable f, Ord a) =>
MatchF c f v a -> a
elem :: forall a. Eq a => a -> MatchF c f v a -> Bool
$celem :: forall c (f :: * -> *) v a.
(Foldable f, Eq a) =>
a -> MatchF c f v a -> Bool
length :: forall a. MatchF c f v a -> Int
$clength :: forall c (f :: * -> *) v a. Foldable f => MatchF c f v a -> Int
null :: forall a. MatchF c f v a -> Bool
$cnull :: forall c (f :: * -> *) v a. Foldable f => MatchF c f v a -> Bool
toList :: forall a. MatchF c f v a -> [a]
$ctoList :: forall c (f :: * -> *) v a. Foldable f => MatchF c f v a -> [a]
foldl1 :: forall a. (a -> a -> a) -> MatchF c f v a -> a
$cfoldl1 :: forall c (f :: * -> *) v a.
Foldable f =>
(a -> a -> a) -> MatchF c f v a -> a
foldr1 :: forall a. (a -> a -> a) -> MatchF c f v a -> a
$cfoldr1 :: forall c (f :: * -> *) v a.
Foldable f =>
(a -> a -> a) -> MatchF c f v a -> a
foldl' :: forall b a. (b -> a -> b) -> b -> MatchF c f v a -> b
$cfoldl' :: forall c (f :: * -> *) v b a.
Foldable f =>
(b -> a -> b) -> b -> MatchF c f v a -> b
foldl :: forall b a. (b -> a -> b) -> b -> MatchF c f v a -> b
$cfoldl :: forall c (f :: * -> *) v b a.
Foldable f =>
(b -> a -> b) -> b -> MatchF c f v a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> MatchF c f v a -> b
$cfoldr' :: forall c (f :: * -> *) v a b.
Foldable f =>
(a -> b -> b) -> b -> MatchF c f v a -> b
foldr :: forall a b. (a -> b -> b) -> b -> MatchF c f v a -> b
$cfoldr :: forall c (f :: * -> *) v a b.
Foldable f =>
(a -> b -> b) -> b -> MatchF c f v a -> b
foldMap' :: forall m a. Monoid m => (a -> m) -> MatchF c f v a -> m
$cfoldMap' :: forall c (f :: * -> *) v m a.
(Foldable f, Monoid m) =>
(a -> m) -> MatchF c f v a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> MatchF c f v a -> m
$cfoldMap :: forall c (f :: * -> *) v m a.
(Foldable f, Monoid m) =>
(a -> m) -> MatchF c f v a -> m
fold :: forall m. Monoid m => MatchF c f v m -> m
$cfold :: forall c (f :: * -> *) v m.
(Foldable f, Monoid m) =>
MatchF c f v m -> m
Foldable, forall {c} {f :: * -> *} {v}.
Traversable f =>
Functor (MatchF c f v)
forall {c} {f :: * -> *} {v}.
Traversable f =>
Foldable (MatchF c f v)
forall c (f :: * -> *) v (m :: * -> *) a.
(Traversable f, Monad m) =>
MatchF c f v (m a) -> m (MatchF c f v a)
forall c (f :: * -> *) v (f :: * -> *) a.
(Traversable f, Applicative f) =>
MatchF c f v (f a) -> f (MatchF c f v a)
forall c (f :: * -> *) v (m :: * -> *) a b.
(Traversable f, Monad m) =>
(a -> m b) -> MatchF c f v a -> m (MatchF c f v b)
forall c (f :: * -> *) v (f :: * -> *) a b.
(Traversable f, Applicative f) =>
(a -> f b) -> MatchF c f v a -> f (MatchF c f v b)
forall (t :: * -> *).
Functor t
-> Foldable t
-> (forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> MatchF c f v a -> f (MatchF c f v b)
sequence :: forall (m :: * -> *) a.
Monad m =>
MatchF c f v (m a) -> m (MatchF c f v a)
$csequence :: forall c (f :: * -> *) v (m :: * -> *) a.
(Traversable f, Monad m) =>
MatchF c f v (m a) -> m (MatchF c f v a)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> MatchF c f v a -> m (MatchF c f v b)
$cmapM :: forall c (f :: * -> *) v (m :: * -> *) a b.
(Traversable f, Monad m) =>
(a -> m b) -> MatchF c f v a -> m (MatchF c f v b)
sequenceA :: forall (f :: * -> *) a.
Applicative f =>
MatchF c f v (f a) -> f (MatchF c f v a)
$csequenceA :: forall c (f :: * -> *) v (f :: * -> *) a.
(Traversable f, Applicative f) =>
MatchF c f v (f a) -> f (MatchF c f v a)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> MatchF c f v a -> f (MatchF c f v b)
$ctraverse :: forall c (f :: * -> *) v (f :: * -> *) a b.
(Traversable f, Applicative f) =>
(a -> f b) -> MatchF c f v a -> f (MatchF c f v b)
Traversable)

-- | Tie the knot - the inner part of 'MatchF'.
data MatchPatF f v r =
    MatchPatPureF !v
  | MatchPatEmbedF !(f r)
  deriving stock (forall a b. a -> MatchPatF f v b -> MatchPatF f v a
forall a b. (a -> b) -> MatchPatF f v a -> MatchPatF f v b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
forall (f :: * -> *) v a b.
Functor f =>
a -> MatchPatF f v b -> MatchPatF f v a
forall (f :: * -> *) v a b.
Functor f =>
(a -> b) -> MatchPatF f v a -> MatchPatF f v b
<$ :: forall a b. a -> MatchPatF f v b -> MatchPatF f v a
$c<$ :: forall (f :: * -> *) v a b.
Functor f =>
a -> MatchPatF f v b -> MatchPatF f v a
fmap :: forall a b. (a -> b) -> MatchPatF f v a -> MatchPatF f v b
$cfmap :: forall (f :: * -> *) v a b.
Functor f =>
(a -> b) -> MatchPatF f v a -> MatchPatF f v b
Functor, forall a. MatchPatF f v a -> Bool
forall m a. Monoid m => (a -> m) -> MatchPatF f v a -> m
forall a b. (a -> b -> b) -> b -> MatchPatF f v a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
forall (f :: * -> *) v a.
(Foldable f, Eq a) =>
a -> MatchPatF f v a -> Bool
forall (f :: * -> *) v a.
(Foldable f, Num a) =>
MatchPatF f v a -> a
forall (f :: * -> *) v a.
(Foldable f, Ord a) =>
MatchPatF f v a -> a
forall (f :: * -> *) v m.
(Foldable f, Monoid m) =>
MatchPatF f v m -> m
forall (f :: * -> *) v a. Foldable f => MatchPatF f v a -> Bool
forall (f :: * -> *) v a. Foldable f => MatchPatF f v a -> Int
forall (f :: * -> *) v a. Foldable f => MatchPatF f v a -> [a]
forall (f :: * -> *) v a.
Foldable f =>
(a -> a -> a) -> MatchPatF f v a -> a
forall (f :: * -> *) v m a.
(Foldable f, Monoid m) =>
(a -> m) -> MatchPatF f v a -> m
forall (f :: * -> *) v b a.
Foldable f =>
(b -> a -> b) -> b -> MatchPatF f v a -> b
forall (f :: * -> *) v a b.
Foldable f =>
(a -> b -> b) -> b -> MatchPatF f v a -> b
product :: forall a. Num a => MatchPatF f v a -> a
$cproduct :: forall (f :: * -> *) v a.
(Foldable f, Num a) =>
MatchPatF f v a -> a
sum :: forall a. Num a => MatchPatF f v a -> a
$csum :: forall (f :: * -> *) v a.
(Foldable f, Num a) =>
MatchPatF f v a -> a
minimum :: forall a. Ord a => MatchPatF f v a -> a
$cminimum :: forall (f :: * -> *) v a.
(Foldable f, Ord a) =>
MatchPatF f v a -> a
maximum :: forall a. Ord a => MatchPatF f v a -> a
$cmaximum :: forall (f :: * -> *) v a.
(Foldable f, Ord a) =>
MatchPatF f v a -> a
elem :: forall a. Eq a => a -> MatchPatF f v a -> Bool
$celem :: forall (f :: * -> *) v a.
(Foldable f, Eq a) =>
a -> MatchPatF f v a -> Bool
length :: forall a. MatchPatF f v a -> Int
$clength :: forall (f :: * -> *) v a. Foldable f => MatchPatF f v a -> Int
null :: forall a. MatchPatF f v a -> Bool
$cnull :: forall (f :: * -> *) v a. Foldable f => MatchPatF f v a -> Bool
toList :: forall a. MatchPatF f v a -> [a]
$ctoList :: forall (f :: * -> *) v a. Foldable f => MatchPatF f v a -> [a]
foldl1 :: forall a. (a -> a -> a) -> MatchPatF f v a -> a
$cfoldl1 :: forall (f :: * -> *) v a.
Foldable f =>
(a -> a -> a) -> MatchPatF f v a -> a
foldr1 :: forall a. (a -> a -> a) -> MatchPatF f v a -> a
$cfoldr1 :: forall (f :: * -> *) v a.
Foldable f =>
(a -> a -> a) -> MatchPatF f v a -> a
foldl' :: forall b a. (b -> a -> b) -> b -> MatchPatF f v a -> b
$cfoldl' :: forall (f :: * -> *) v b a.
Foldable f =>
(b -> a -> b) -> b -> MatchPatF f v a -> b
foldl :: forall b a. (b -> a -> b) -> b -> MatchPatF f v a -> b
$cfoldl :: forall (f :: * -> *) v b a.
Foldable f =>
(b -> a -> b) -> b -> MatchPatF f v a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> MatchPatF f v a -> b
$cfoldr' :: forall (f :: * -> *) v a b.
Foldable f =>
(a -> b -> b) -> b -> MatchPatF f v a -> b
foldr :: forall a b. (a -> b -> b) -> b -> MatchPatF f v a -> b
$cfoldr :: forall (f :: * -> *) v a b.
Foldable f =>
(a -> b -> b) -> b -> MatchPatF f v a -> b
foldMap' :: forall m a. Monoid m => (a -> m) -> MatchPatF f v a -> m
$cfoldMap' :: forall (f :: * -> *) v m a.
(Foldable f, Monoid m) =>
(a -> m) -> MatchPatF f v a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> MatchPatF f v a -> m
$cfoldMap :: forall (f :: * -> *) v m a.
(Foldable f, Monoid m) =>
(a -> m) -> MatchPatF f v a -> m
fold :: forall m. Monoid m => MatchPatF f v m -> m
$cfold :: forall (f :: * -> *) v m.
(Foldable f, Monoid m) =>
MatchPatF f v m -> m
Foldable, forall (t :: * -> *).
Functor t
-> Foldable t
-> (forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall {f :: * -> *} {v}. Traversable f => Functor (MatchPatF f v)
forall {f :: * -> *} {v}. Traversable f => Foldable (MatchPatF f v)
forall (f :: * -> *) v (m :: * -> *) a.
(Traversable f, Monad m) =>
MatchPatF f v (m a) -> m (MatchPatF f v a)
forall (f :: * -> *) v (f :: * -> *) a.
(Traversable f, Applicative f) =>
MatchPatF f v (f a) -> f (MatchPatF f v a)
forall (f :: * -> *) v (m :: * -> *) a b.
(Traversable f, Monad m) =>
(a -> m b) -> MatchPatF f v a -> m (MatchPatF f v b)
forall (f :: * -> *) v (f :: * -> *) a b.
(Traversable f, Applicative f) =>
(a -> f b) -> MatchPatF f v a -> f (MatchPatF f v b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> MatchPatF f v a -> f (MatchPatF f v b)
sequence :: forall (m :: * -> *) a.
Monad m =>
MatchPatF f v (m a) -> m (MatchPatF f v a)
$csequence :: forall (f :: * -> *) v (m :: * -> *) a.
(Traversable f, Monad m) =>
MatchPatF f v (m a) -> m (MatchPatF f v a)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> MatchPatF f v a -> m (MatchPatF f v b)
$cmapM :: forall (f :: * -> *) v (m :: * -> *) a b.
(Traversable f, Monad m) =>
(a -> m b) -> MatchPatF f v a -> m (MatchPatF f v b)
sequenceA :: forall (f :: * -> *) a.
Applicative f =>
MatchPatF f v (f a) -> f (MatchPatF f v a)
$csequenceA :: forall (f :: * -> *) v (f :: * -> *) a.
(Traversable f, Applicative f) =>
MatchPatF f v (f a) -> f (MatchPatF f v a)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> MatchPatF f v a -> f (MatchPatF f v b)
$ctraverse :: forall (f :: * -> *) v (f :: * -> *) a b.
(Traversable f, Applicative f) =>
(a -> f b) -> MatchPatF f v a -> f (MatchPatF f v b)
Traversable)

type instance Base (Match c f v) = MatchF c f v

instance Functor f => Recursive (Match c f v) where
  project :: Match c f v -> Base (Match c f v) (Match c f v)
project (Match c
cl MatchPat c f v
mp) = forall c (f :: * -> *) v r. c -> MatchPatF f v r -> MatchF c f v r
MatchF c
cl forall a b. (a -> b) -> a -> b
$ case MatchPat c f v
mp of
     MatchPatPure v
v -> forall (f :: * -> *) v r. v -> MatchPatF f v r
MatchPatPureF v
v
     MatchPatEmbed f (Match c f v)
f -> forall (f :: * -> *) v r. f r -> MatchPatF f v r
MatchPatEmbedF f (Match c f v)
f

instance Functor f => Corecursive (Match c f v) where
  embed :: Base (Match c f v) (Match c f v) -> Match c f v
embed (MatchF c
cl MatchPatF f v (Match c f v)
mpf) = forall c (f :: * -> *) v. c -> MatchPat c f v -> Match c f v
Match c
cl forall a b. (a -> b) -> a -> b
$ case MatchPatF f v (Match c f v)
mpf of
     MatchPatPureF v
v -> forall c (f :: * -> *) v. v -> MatchPat c f v
MatchPatPure v
v
     MatchPatEmbedF f (Match c f v)
f -> forall c (f :: * -> *) v. f (Match c f v) -> MatchPat c f v
MatchPatEmbed f (Match c f v)
f

-- | The set of vars in a match.
matchVars :: (Foldable f, Eq v, Hashable v) => Match c f v -> HashSet v
matchVars :: forall (f :: * -> *) v c.
(Foldable f, Eq v, Hashable v) =>
Match c f v -> HashSet v
matchVars = forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap' forall a. Hashable a => a -> HashSet a
HashSet.singleton

-- | The set of classes in a match.
matchClasses :: (Coercible c Int, Functor f, Foldable f) => Match c f v -> IntLikeSet c
matchClasses :: forall c (f :: * -> *) v.
(Coercible c Int, Functor f, Foldable f) =>
Match c f v -> IntLikeSet c
matchClasses = forall t a. Recursive t => (Base t a -> a) -> t -> a
cata forall {x} {t :: * -> *} {v}.
(Coercible x Int, Foldable t) =>
MatchF x t v (IntLikeSet x) -> IntLikeSet x
go where
  go :: MatchF x t v (IntLikeSet x) -> IntLikeSet x
go (MatchF x
cl MatchPatF t v (IntLikeSet x)
mpf) = forall x. Coercible x Int => x -> IntLikeSet x -> IntLikeSet x
ILS.insert x
cl forall a b. (a -> b) -> a -> b
$ case MatchPatF t v (IntLikeSet x)
mpf of
    MatchPatPureF v
_ -> forall x. IntLikeSet x
ILS.empty
    MatchPatEmbedF t (IntLikeSet x)
fc -> forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold t (IntLikeSet x)
fc

-- | A apri of match and substitution.
data MatchSubst c f v = MatchSubst
  { forall c (f :: * -> *) v. MatchSubst c f v -> Match c f v
msMatch :: !(Match c f v)
  , forall c (f :: * -> *) v. MatchSubst c f v -> Subst c v
msSubst :: !(Subst c v)
  }

deriving stock instance (Eq c, Eq v, Eq (f (Match c f v))) => Eq (MatchSubst c f v)
deriving stock instance (Show c, Show v, Show (f (Match c f v))) => Show (MatchSubst c f v)

-- | An opaque var id
-- Constructor exported for coercibility
newtype VarId = VarId { VarId -> Int
unVarId :: Int }
  deriving stock (Int -> VarId -> ShowS
[VarId] -> ShowS
VarId -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [VarId] -> ShowS
$cshowList :: [VarId] -> ShowS
show :: VarId -> String
$cshow :: VarId -> String
showsPrec :: Int -> VarId -> ShowS
$cshowsPrec :: Int -> VarId -> ShowS
Show)
  deriving newtype (VarId -> VarId -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: VarId -> VarId -> Bool
$c/= :: VarId -> VarId -> Bool
== :: VarId -> VarId -> Bool
$c== :: VarId -> VarId -> Bool
Eq, Eq VarId
VarId -> VarId -> Bool
VarId -> VarId -> Ordering
VarId -> VarId -> VarId
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: VarId -> VarId -> VarId
$cmin :: VarId -> VarId -> VarId
max :: VarId -> VarId -> VarId
$cmax :: VarId -> VarId -> VarId
>= :: VarId -> VarId -> Bool
$c>= :: VarId -> VarId -> Bool
> :: VarId -> VarId -> Bool
$c> :: VarId -> VarId -> Bool
<= :: VarId -> VarId -> Bool
$c<= :: VarId -> VarId -> Bool
< :: VarId -> VarId -> Bool
$c< :: VarId -> VarId -> Bool
compare :: VarId -> VarId -> Ordering
$ccompare :: VarId -> VarId -> Ordering
Ord, Int -> VarId
VarId -> Int
VarId -> [VarId]
VarId -> VarId
VarId -> VarId -> [VarId]
VarId -> VarId -> VarId -> [VarId]
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
enumFromThenTo :: VarId -> VarId -> VarId -> [VarId]
$cenumFromThenTo :: VarId -> VarId -> VarId -> [VarId]
enumFromTo :: VarId -> VarId -> [VarId]
$cenumFromTo :: VarId -> VarId -> [VarId]
enumFromThen :: VarId -> VarId -> [VarId]
$cenumFromThen :: VarId -> VarId -> [VarId]
enumFrom :: VarId -> [VarId]
$cenumFrom :: VarId -> [VarId]
fromEnum :: VarId -> Int
$cfromEnum :: VarId -> Int
toEnum :: Int -> VarId
$ctoEnum :: Int -> VarId
pred :: VarId -> VarId
$cpred :: VarId -> VarId
succ :: VarId -> VarId
$csucc :: VarId -> VarId
Enum, Eq VarId
Int -> VarId -> Int
VarId -> Int
forall a. Eq a -> (Int -> a -> Int) -> (a -> Int) -> Hashable a
hash :: VarId -> Int
$chash :: VarId -> Int
hashWithSalt :: Int -> VarId -> Int
$chashWithSalt :: Int -> VarId -> Int
Hashable, VarId -> ()
forall a. (a -> ()) -> NFData a
rnf :: VarId -> ()
$crnf :: VarId -> ()
NFData)

-- | A pattern graph - can be created once for each pattern and reused
-- for many iterations of search.
-- 'g' is the pattern group functor.
-- 'f' is the language functor.
data PatGraph g f v = PatGraph
  { forall (g :: * -> *) (f :: * -> *) v. PatGraph g f v -> g VarId
pgRoots :: !(g VarId)
  , forall (g :: * -> *) (f :: * -> *) v.
PatGraph g f v -> IntLikeMap VarId (PatF f v VarId)
pgNodes :: !(IntLikeMap VarId (PatF f v VarId))
  , forall (g :: * -> *) (f :: * -> *) v.
PatGraph g f v -> HashMap v VarId
pgVars :: !(HashMap v VarId)
  }

deriving stock instance (Eq v, Eq (g VarId), Eq (f VarId)) => Eq (PatGraph g f v)
deriving stock instance (Show v, Show (g VarId), Show (f VarId)) => Show (PatGraph g f v)

-- | The set of constraints necessary to build a pattern graph.
type PatGraphC f v = (Traversable f, Traversable f, Eq v, Eq (f VarId), Hashable v, Hashable (f VarId))

data GraphState f v = GraphState
  { forall (f :: * -> *) v. GraphState f v -> Source VarId
gsSrc :: !(Source VarId)
  , forall (f :: * -> *) v.
GraphState f v -> Assoc VarId (PatF f v VarId)
gsAssoc :: !(Assoc VarId (PatF f v VarId))
  }

emptyGraphState :: GraphState f v
emptyGraphState :: forall (f :: * -> *) v. GraphState f v
emptyGraphState = forall (f :: * -> *) v.
Source VarId -> Assoc VarId (PatF f v VarId) -> GraphState f v
GraphState (forall x. Coercible x Int => x -> Source x
sourceNew (Int -> VarId
VarId Int
0)) forall x a. Assoc x a
assocNew

graphEnsurePart :: PatGraphC f v => PatF f v VarId -> State (GraphState f v) VarId
graphEnsurePart :: forall (f :: * -> *) v.
PatGraphC f v =>
PatF f v VarId -> State (GraphState f v) VarId
graphEnsurePart PatF f v VarId
part = do
  Maybe VarId
mi <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets (forall a x. (Eq a, Hashable a) => a -> Assoc x a -> Maybe x
assocLookupByValue PatF f v VarId
part forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) v.
GraphState f v -> Assoc VarId (PatF f v VarId)
gsAssoc)
  case Maybe VarId
mi of
    Just VarId
i -> forall (f :: * -> *) a. Applicative f => a -> f a
pure VarId
i
    Maybe VarId
Nothing -> forall s (m :: * -> *) a. MonadState s m => (s -> (a, s)) -> m a
state forall a b. (a -> b) -> a -> b
$ \GraphState f v
st ->
      let (VarId
i, Source VarId
src') = forall x. Coercible x Int => Source x -> (x, Source x)
sourceAddInc (forall (f :: * -> *) v. GraphState f v -> Source VarId
gsSrc GraphState f v
st)
          ((VarId, AssocInsertRes VarId)
_, Assoc VarId (PatF f v VarId)
assoc') = forall x a.
(Coercible x Int, Ord x, Eq a, Hashable a) =>
x -> a -> Assoc x a -> ((x, AssocInsertRes x), Assoc x a)
assocInsertInc VarId
i PatF f v VarId
part (forall (f :: * -> *) v.
GraphState f v -> Assoc VarId (PatF f v VarId)
gsAssoc GraphState f v
st)
      in (VarId
i, GraphState f v
st { gsSrc :: Source VarId
gsSrc = Source VarId
src', gsAssoc :: Assoc VarId (PatF f v VarId)
gsAssoc = Assoc VarId (PatF f v VarId)
assoc' })

graphEnsurePat :: PatGraphC f v => Pat f v -> State (GraphState f v) VarId
graphEnsurePat :: forall (f :: * -> *) v.
PatGraphC f v =>
Pat f v -> State (GraphState f v) VarId
graphEnsurePat = forall t a. Recursive t => (Base t a -> a) -> t -> a
cata FreeF f v (StateT (GraphState f v) Identity VarId)
-> StateT (GraphState f v) Identity VarId
go where
  go :: FreeF f v (StateT (GraphState f v) Identity VarId)
-> StateT (GraphState f v) Identity VarId
go = \case
    FreePureF v
v -> forall (f :: * -> *) v.
PatGraphC f v =>
PatF f v VarId -> State (GraphState f v) VarId
graphEnsurePart (forall (f :: * -> *) a r. a -> FreeF f a r
FreePureF v
v)
    FreeEmbedF f (StateT (GraphState f v) Identity VarId)
fp -> do
      f VarId
fi <- forall (t :: * -> *) (f :: * -> *) a.
(Traversable t, Applicative f) =>
t (f a) -> f (t a)
sequenceA f (StateT (GraphState f v) Identity VarId)
fp
      forall (f :: * -> *) v.
PatGraphC f v =>
PatF f v VarId -> State (GraphState f v) VarId
graphEnsurePart (forall (f :: * -> *) a r. f r -> FreeF f a r
FreeEmbedF f VarId
fi)

graphCanonicalize :: PatGraphC f v => GraphState f v -> IntLikeMap VarId (PatF f v VarId)
graphCanonicalize :: forall (f :: * -> *) v.
PatGraphC f v =>
GraphState f v -> IntLikeMap VarId (PatF f v VarId)
graphCanonicalize (GraphState Source VarId
_ Assoc VarId (PatF f v VarId)
assoc) =
  let fwd :: IntLikeMap VarId (PatF f v VarId)
fwd = forall x a. Assoc x a -> IntLikeMap x a
assocFwd Assoc VarId (PatF f v VarId)
assoc
      equiv :: EquivFind VarId
equiv = forall x a. Assoc x a -> EquivFind x
assocEquiv Assoc VarId (PatF f v VarId)
assoc
  in forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall x. Coercible x Int => x -> EquivFind x -> x
`efLookupRoot` EquivFind VarId
equiv)) IntLikeMap VarId (PatF f v VarId)
fwd

-- | Builds a pattern graph from a group of patterns.
patGraph :: (Traversable g, PatGraphC f v) => PatGroup g f v -> PatGraph g f v
patGraph :: forall (g :: * -> *) (f :: * -> *) v.
(Traversable g, PatGraphC f v) =>
PatGroup g f v -> PatGraph g f v
patGraph PatGroup g f v
ps =
  let (g VarId
gr, GraphState f v
st) = forall s a. State s a -> s -> (a, s)
runState (forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall (f :: * -> *) v.
PatGraphC f v =>
Pat f v -> State (GraphState f v) VarId
graphEnsurePat PatGroup g f v
ps) forall (f :: * -> *) v. GraphState f v
emptyGraphState
      m :: IntLikeMap VarId (PatF f v VarId)
m = forall (f :: * -> *) v.
PatGraphC f v =>
GraphState f v -> IntLikeMap VarId (PatF f v VarId)
graphCanonicalize GraphState f v
st
      n :: HashMap v VarId
n = forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
HashMap.fromList (forall x a. Coercible x Int => IntLikeMap x a -> [(x, a)]
ILM.toList IntLikeMap VarId (PatF f v VarId)
m forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \(VarId
j, PatF f v VarId
x) -> case PatF f v VarId
x of { FreePureF v
v -> [(v
v, VarId
j)]; PatF f v VarId
_ -> [] })
  in forall (g :: * -> *) (f :: * -> *) v.
g VarId
-> IntLikeMap VarId (PatF f v VarId)
-> HashMap v VarId
-> PatGraph g f v
PatGraph g VarId
gr IntLikeMap VarId (PatF f v VarId)
m HashMap v VarId
n

-- | Builds a pattern graph from a single pattern.
-- If you have more than one pattern, building the group all at once is going to
-- make finding solutions more efficient.
singlePatGraph :: PatGraphC f v => Pat f v -> PatGraph Identity f v
singlePatGraph :: forall (f :: * -> *) v.
PatGraphC f v =>
Pat f v -> PatGraph Identity f v
singlePatGraph = forall (g :: * -> *) (f :: * -> *) v.
(Traversable g, PatGraphC f v) =>
PatGroup g f v -> PatGraph g f v
patGraph forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> Identity a
Identity

-- | A solution graph - must be created from an e-graph each merge/rebuild.
data SolGraph c f = SolGraph
  { forall c (f :: * -> *).
SolGraph c f -> IntLikeMap VarId (IntLikeSet c)
sgByVar :: !(IntLikeMap VarId (IntLikeSet c))
  -- ^ Map of var -> classes.
  -- Contains all vars.
  -- If the inner map is empty, that means the pattern was not matched.
  -- The inner set will not be empty.
  , forall c (f :: * -> *). SolGraph c f -> HashMap (f c) c
sgNodes :: !(HashMap (f c) c)
  -- ^ Map of node structures to classes.
  }

deriving stock instance (Eq c, Eq (f c)) => Eq (SolGraph c f)
deriving stock instance (Show c, Show (f c)) => Show (SolGraph c f)

-- | The set of constraints necessary to build a solution graph.
type SolGraphC f = (Functor f, Foldable f, Eq (f ()), Hashable (f ()))

-- | Builds a solution graph from an e-graph.
solGraph :: SolGraphC f => PatGraph g f v -> EGraph d f -> SolGraph EClassId f
solGraph :: forall (f :: * -> *) (g :: * -> *) v d.
SolGraphC f =>
PatGraph g f v -> EGraph d f -> SolGraph EClassId f
solGraph PatGraph g f v
pg EGraph d f
eg =
  -- For each class, use footprint of reverse node assoc to find set of node ids
  -- Start with just the embedded nodes
  let byVarEmbed :: IntLikeMap VarId (IntLikeSet EClassId, IntLikeSet ENodeId)
byVarEmbed = forall x a. Coercible x Int => [(x, a)] -> IntLikeMap x a
ILM.fromList forall a b. (a -> b) -> a -> b
$ forall x a. Coercible x Int => IntLikeMap x a -> [(x, a)]
ILM.toList (forall (g :: * -> *) (f :: * -> *) v.
PatGraph g f v -> IntLikeMap VarId (PatF f v VarId)
pgNodes PatGraph g f v
pg) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \(VarId
i, PatF f v VarId
pf) ->
        case PatF f v VarId
pf of
          FreePureF v
_ -> []
          FreeEmbedF f VarId
fi ->
            let fu :: f ()
fu = forall (f :: * -> *) a. Functor f => f a -> f ()
void f VarId
fi
                cns :: [(EClassId, IntLikeSet ENodeId)]
cns = forall x a. Coercible x Int => IntLikeMap x a -> [(x, a)]
ILM.toList (forall d (f :: * -> *).
EGraph d f -> IntLikeMap EClassId (EClassInfo d f)
egClassMap EGraph d f
eg) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \(EClassId
c, EClassInfo d f
inf) ->
                  let ns :: Assoc ENodeId (f ())
ns = forall d (f :: * -> *). EClassInfo d f -> Assoc ENodeId (f ())
eciNodes EClassInfo d f
inf
                      fp :: IntLikeSet ENodeId
fp = forall x a.
(Coercible x Int, Eq a, Hashable a) =>
a -> Assoc x a -> IntLikeSet x
assocFootprint f ()
fu Assoc ENodeId (f ())
ns
                  in [(EClassId
c, IntLikeSet ENodeId
fp) | Bool -> Bool
not (forall x. IntLikeSet x -> Bool
ILS.null IntLikeSet ENodeId
fp)]
            in [(VarId
i, forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap forall x. Coercible x Int => [x] -> IntLikeSet x
ILS.fromList forall a. Monoid a => [a] -> a
mconcat (forall a b. [(a, b)] -> ([a], [b])
unzip [(EClassId, IntLikeSet ENodeId)]
cns))]
      byVar :: IntLikeMap VarId (IntLikeSet EClassId)
byVar = forall (f :: * -> *) v.
Foldable f =>
IntLikeMap VarId (IntLikeSet EClassId, IntLikeSet ENodeId)
-> IntLikeMap VarId (PatF f v VarId)
-> IntLikeMap ENodeId (f EClassId)
-> IntLikeMap VarId (IntLikeSet EClassId)
genByVar IntLikeMap VarId (IntLikeSet EClassId, IntLikeSet ENodeId)
byVarEmbed (forall (g :: * -> *) (f :: * -> *) v.
PatGraph g f v -> IntLikeMap VarId (PatF f v VarId)
pgNodes PatGraph g f v
pg) (forall x a. Assoc x a -> IntLikeMap x a
assocFwd (forall d (f :: * -> *). EGraph d f -> Assoc ENodeId (f EClassId)
egNodeAssoc EGraph d f
eg))
      hc :: IntLikeMap ENodeId EClassId
hc = forall d (f :: * -> *). EGraph d f -> IntLikeMap ENodeId EClassId
egHashCons EGraph d f
eg
      nodes :: HashMap (f EClassId) EClassId
nodes = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall x a. Coercible x Int => x -> IntLikeMap x a -> a
`ILM.partialLookup` IntLikeMap ENodeId EClassId
hc) (forall x a. Assoc x a -> HashMap a x
assocBwd (forall d (f :: * -> *). EGraph d f -> Assoc ENodeId (f EClassId)
egNodeAssoc EGraph d f
eg))
  in forall c (f :: * -> *).
IntLikeMap VarId (IntLikeSet c) -> HashMap (f c) c -> SolGraph c f
SolGraph IntLikeMap VarId (IntLikeSet EClassId)
byVar HashMap (f EClassId) EClassId
nodes

data Record =
    RecordPure !VarId !(IntLikeSet EClassId)
  | RecordEmbed
  deriving stock (Record -> Record -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Record -> Record -> Bool
$c/= :: Record -> Record -> Bool
== :: Record -> Record -> Bool
$c== :: Record -> Record -> Bool
Eq, Int -> Record -> ShowS
[Record] -> ShowS
Record -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Record] -> ShowS
$cshowList :: [Record] -> ShowS
show :: Record -> String
$cshow :: Record -> String
showsPrec :: Int -> Record -> ShowS
$cshowsPrec :: Int -> Record -> ShowS
Show)

type Records = [Record]

initRecords :: Foldable f => IntLikeMap VarId (PatF f v VarId) -> f VarId -> Records
initRecords :: forall (f :: * -> *) v.
Foldable f =>
IntLikeMap VarId (PatF f v VarId) -> f VarId -> [Record]
initRecords IntLikeMap VarId (PatF f v VarId)
nodes = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\VarId
i -> case forall x a. Coercible x Int => x -> IntLikeMap x a -> a
ILM.partialLookup VarId
i IntLikeMap VarId (PatF f v VarId)
nodes of { FreePureF v
_ -> VarId -> IntLikeSet EClassId -> Record
RecordPure VarId
i forall x. IntLikeSet x
ILS.empty; PatF f v VarId
_ -> Record
RecordEmbed }) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a. Foldable t => t a -> [a]
toList

updateRecords :: Foldable f => Records -> f EClassId -> Records
updateRecords :: forall (f :: * -> *).
Foldable f =>
[Record] -> f EClassId -> [Record]
updateRecords [Record]
rs = forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\Record
r EClassId
c -> case Record
r of { RecordPure VarId
v IntLikeSet EClassId
cs -> VarId -> IntLikeSet EClassId -> Record
RecordPure VarId
v (forall x. Coercible x Int => x -> IntLikeSet x -> IntLikeSet x
ILS.insert EClassId
c IntLikeSet EClassId
cs); Record
_ -> Record
r } ) [Record]
rs forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a. Foldable t => t a -> [a]
toList

genByVar :: Foldable f => IntLikeMap VarId (IntLikeSet EClassId, IntLikeSet ENodeId) -> IntLikeMap VarId (PatF f v VarId) -> IntLikeMap ENodeId (f EClassId) -> IntLikeMap VarId (IntLikeSet EClassId)
genByVar :: forall (f :: * -> *) v.
Foldable f =>
IntLikeMap VarId (IntLikeSet EClassId, IntLikeSet ENodeId)
-> IntLikeMap VarId (PatF f v VarId)
-> IntLikeMap ENodeId (f EClassId)
-> IntLikeMap VarId (IntLikeSet EClassId)
genByVar IntLikeMap VarId (IntLikeSet EClassId, IntLikeSet ENodeId)
byVarEmbed IntLikeMap VarId (PatF f v VarId)
nodes IntLikeMap ENodeId (f EClassId)
fwd = forall s a. State s a -> s -> s
execState (forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
t a -> (a -> f b) -> f ()
for_ (forall x a. Coercible x Int => IntLikeMap x a -> [(x, a)]
ILM.toList IntLikeMap VarId (PatF f v VarId)
nodes) (VarId, PatF f v VarId)
-> StateT (IntLikeMap VarId (IntLikeSet EClassId)) Identity ()
go) (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. (a, b) -> a
fst IntLikeMap VarId (IntLikeSet EClassId, IntLikeSet ENodeId)
byVarEmbed) where
  go :: (VarId, PatF f v VarId)
-> StateT (IntLikeMap VarId (IntLikeSet EClassId)) Identity ()
go (VarId
i, PatF f v VarId
pf) =
    case PatF f v VarId
pf of
      FreePureF v
_ -> forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
      FreeEmbedF f VarId
fi -> do
        -- We've gone through embedded patterns before so we're able
        -- to look up nodes for each pattern
        let (IntLikeSet EClassId
_, IntLikeSet ENodeId
ns) = forall x a. Coercible x Int => x -> IntLikeMap x a -> a
ILM.partialLookup VarId
i IntLikeMap VarId (IntLikeSet EClassId, IntLikeSet ENodeId)
byVarEmbed
        -- For each node, update positionally what it could be
        let rs :: [Record]
rs = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (\[Record]
rsx ENodeId
n -> let fc :: f EClassId
fc = forall x a. Coercible x Int => x -> IntLikeMap x a -> a
ILM.partialLookup ENodeId
n IntLikeMap ENodeId (f EClassId)
fwd in forall (f :: * -> *).
Foldable f =>
[Record] -> f EClassId -> [Record]
updateRecords [Record]
rsx f EClassId
fc) (forall (f :: * -> *) v.
Foldable f =>
IntLikeMap VarId (PatF f v VarId) -> f VarId -> [Record]
initRecords IntLikeMap VarId (PatF f v VarId)
nodes f VarId
fi) (forall x. Coercible x Int => IntLikeSet x -> [x]
ILS.toList IntLikeSet ENodeId
ns)
        -- Finally update the map; if missing set the positions as is, otherwise take intersection
        forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify' forall a b. (a -> b) -> a -> b
$ \IntLikeMap VarId (IntLikeSet EClassId)
m -> forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (\IntLikeMap VarId (IntLikeSet EClassId)
mx Record
r -> case Record
r of {RecordPure VarId
j IntLikeSet EClassId
cs -> forall x a.
Coercible x Int =>
(Maybe a -> Maybe a) -> x -> IntLikeMap x a -> IntLikeMap x a
ILM.alter (forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall b a. b -> (a -> b) -> Maybe a -> b
maybe IntLikeSet EClassId
cs (forall x. IntLikeSet x -> IntLikeSet x -> IntLikeSet x
ILS.intersection IntLikeSet EClassId
cs)) VarId
j IntLikeMap VarId (IntLikeSet EClassId)
mx; Record
_ -> IntLikeMap VarId (IntLikeSet EClassId)
mx}) IntLikeMap VarId (IntLikeSet EClassId)
m [Record]
rs

data SolEnv c g f v = SolEnv
  { forall c (g :: * -> *) (f :: * -> *) v.
SolEnv c g f v -> PatGraph g f v
sePatGraph :: !(PatGraph g f v)
  , forall c (g :: * -> *) (f :: * -> *) v.
SolEnv c g f v -> SolGraph c f
seSolGraph :: !(SolGraph c f)
  }

newtype SolState c = SolState
  { forall c. SolState c -> IntLikeMap VarId c
ssClasses :: IntLikeMap VarId c
  } deriving (SolState c -> SolState c -> Bool
forall c. Eq c => SolState c -> SolState c -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: SolState c -> SolState c -> Bool
$c/= :: forall c. Eq c => SolState c -> SolState c -> Bool
== :: SolState c -> SolState c -> Bool
$c== :: forall c. Eq c => SolState c -> SolState c -> Bool
Eq, Int -> SolState c -> ShowS
forall c. Show c => Int -> SolState c -> ShowS
forall c. Show c => [SolState c] -> ShowS
forall c. Show c => SolState c -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [SolState c] -> ShowS
$cshowList :: forall c. Show c => [SolState c] -> ShowS
show :: SolState c -> String
$cshow :: forall c. Show c => SolState c -> String
showsPrec :: Int -> SolState c -> ShowS
$cshowsPrec :: forall c. Show c => Int -> SolState c -> ShowS
Show)

-- | A stream of solutions. Can be demanded all at once or interleaved.
type SolStream c g f v z = Stream (SolEnv c g f v) (SolState c) z

-- | The set of constraints necessary to search for solutions.
type SolveC c f v = (Traversable f, Coercible c Int, Eq v, Hashable v, Eq (f c), Hashable (f c))

constructMatch :: Traversable f => IntLikeMap VarId (PatF f v VarId) -> IntLikeMap VarId c -> VarId -> Match c f v
constructMatch :: forall (f :: * -> *) v c.
Traversable f =>
IntLikeMap VarId (PatF f v VarId)
-> IntLikeMap VarId c -> VarId -> Match c f v
constructMatch IntLikeMap VarId (PatF f v VarId)
nodes IntLikeMap VarId c
classes VarId
i0 = forall s a. State s a -> s -> a
evalState (VarId
-> StateT (IntLikeMap VarId (Match c f v)) Identity (Match c f v)
go VarId
i0) forall x a. IntLikeMap x a
ILM.empty where
  go :: VarId
-> StateT (IntLikeMap VarId (Match c f v)) Identity (Match c f v)
go VarId
i = do
    IntLikeMap VarId (Match c f v)
cache <- forall s (m :: * -> *). MonadState s m => m s
get
    case forall x a. Coercible x Int => x -> IntLikeMap x a -> Maybe a
ILM.lookup VarId
i IntLikeMap VarId (Match c f v)
cache of
      Just Match c f v
res -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Match c f v
res
      Maybe (Match c f v)
Nothing -> do
        let c :: c
c = forall x a. Coercible x Int => x -> IntLikeMap x a -> a
ILM.partialLookup VarId
i IntLikeMap VarId c
classes
        MatchPat c f v
mp <- case forall x a. Coercible x Int => x -> IntLikeMap x a -> a
ILM.partialLookup VarId
i IntLikeMap VarId (PatF f v VarId)
nodes of
          FreePureF v
v -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$! forall c (f :: * -> *) v. v -> MatchPat c f v
MatchPatPure v
v
          FreeEmbedF f VarId
f -> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall c (f :: * -> *) v. f (Match c f v) -> MatchPat c f v
MatchPatEmbed (forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse VarId
-> StateT (IntLikeMap VarId (Match c f v)) Identity (Match c f v)
go f VarId
f)
        forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$! forall c (f :: * -> *) v. c -> MatchPat c f v -> Match c f v
Match c
c MatchPat c f v
mp

constructSubst :: HashMap v VarId -> IntLikeMap VarId a -> Subst a v
constructSubst :: forall v a. HashMap v VarId -> IntLikeMap VarId a -> Subst a v
constructSubst HashMap v VarId
vars IntLikeMap VarId a
classes = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall x a. Coercible x Int => x -> IntLikeMap x a -> a
`ILM.partialLookup` IntLikeMap VarId a
classes) HashMap v VarId
vars

solveYield :: Traversable f => VarId -> SolStream c g f v (MatchSubst c f v)
solveYield :: forall (f :: * -> *) c (g :: * -> *) v.
Traversable f =>
VarId -> SolStream c g f v (MatchSubst c f v)
solveYield VarId
i = do
  PatGraph g f v
pg <- forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks forall c (g :: * -> *) (f :: * -> *) v.
SolEnv c g f v -> PatGraph g f v
sePatGraph
  IntLikeMap VarId c
classes <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets forall c. SolState c -> IntLikeMap VarId c
ssClasses
  let mat :: Match c f v
mat = forall (f :: * -> *) v c.
Traversable f =>
IntLikeMap VarId (PatF f v VarId)
-> IntLikeMap VarId c -> VarId -> Match c f v
constructMatch (forall (g :: * -> *) (f :: * -> *) v.
PatGraph g f v -> IntLikeMap VarId (PatF f v VarId)
pgNodes PatGraph g f v
pg) IntLikeMap VarId c
classes VarId
i
      subst :: Subst c v
subst = forall v a. HashMap v VarId -> IntLikeMap VarId a -> Subst a v
constructSubst (forall (g :: * -> *) (f :: * -> *) v.
PatGraph g f v -> HashMap v VarId
pgVars PatGraph g f v
pg) IntLikeMap VarId c
classes
      ms :: MatchSubst c f v
ms = forall c (f :: * -> *) v.
Match c f v -> Subst c v -> MatchSubst c f v
MatchSubst Match c f v
mat Subst c v
subst
  forall (f :: * -> *) a. Applicative f => a -> f a
pure MatchSubst c f v
ms

-- | Produces a stream of solutions (e-matches).
solve :: (Foldable g, SolveC c f v) => SolStream c g f v (MatchSubst c f v)
solve :: forall (g :: * -> *) c (f :: * -> *) v.
(Foldable g, SolveC c f v) =>
SolStream c g f v (MatchSubst c f v)
solve = do
  g VarId
roots <- forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks (forall (g :: * -> *) (f :: * -> *) v. PatGraph g f v -> g VarId
pgRoots forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall c (g :: * -> *) (f :: * -> *) v.
SolEnv c g f v -> PatGraph g f v
sePatGraph)
  forall (f :: * -> *) (m :: * -> *) a b.
(Foldable f, Alternative m) =>
f a -> (a -> m b) -> m b
chooseWith g VarId
roots forall a b. (a -> b) -> a -> b
$ \VarId
i -> do
    forall (f :: * -> *) a. Functor f => f a -> f ()
void (forall c (f :: * -> *) v (g :: * -> *).
SolveC c f v =>
VarId -> SolStream c g f v c
solveRec VarId
i)
    forall (f :: * -> *) c (g :: * -> *) v.
Traversable f =>
VarId -> SolStream c g f v (MatchSubst c f v)
solveYield VarId
i

solveChoose :: SolveC c f v => VarId -> IntLikeSet c -> SolStream c g f v c
solveChoose :: forall c (f :: * -> *) v (g :: * -> *).
SolveC c f v =>
VarId -> IntLikeSet c -> SolStream c g f v c
solveChoose VarId
i IntLikeSet c
cs = forall (f :: * -> *) (m :: * -> *) a b.
(Foldable f, Alternative m) =>
f a -> (a -> m b) -> m b
chooseWith (forall x. Coercible x Int => IntLikeSet x -> [x]
ILS.toList IntLikeSet c
cs) (forall c (g :: * -> *) (f :: * -> *) v.
VarId -> c -> SolStream c g f v c
solveSet VarId
i)

solveSet :: VarId -> c -> SolStream c g f v c
solveSet :: forall c (g :: * -> *) (f :: * -> *) v.
VarId -> c -> SolStream c g f v c
solveSet VarId
i c
c =
  c
c forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify' (\SolState c
ss -> SolState c
ss { ssClasses :: IntLikeMap VarId c
ssClasses = forall x a.
Coercible x Int =>
x -> a -> IntLikeMap x a -> IntLikeMap x a
ILM.insert VarId
i c
c (forall c. SolState c -> IntLikeMap VarId c
ssClasses SolState c
ss) })

solveRec :: SolveC c f v => VarId -> SolStream c g f v c
solveRec :: forall c (f :: * -> *) v (g :: * -> *).
SolveC c f v =>
VarId -> SolStream c g f v c
solveRec VarId
i = do
  Maybe c
ms <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets (forall x a. Coercible x Int => x -> IntLikeMap x a -> Maybe a
ILM.lookup VarId
i forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall c. SolState c -> IntLikeMap VarId c
ssClasses)
  case Maybe c
ms of
    -- Seen before, return solution
    Just c
s -> forall (f :: * -> *) a. Applicative f => a -> f a
pure c
s
    -- Unseen
    Maybe c
Nothing -> do
      PatF f v VarId
n <- forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks (forall x a. Coercible x Int => x -> IntLikeMap x a -> a
ILM.partialLookup VarId
i forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (g :: * -> *) (f :: * -> *) v.
PatGraph g f v -> IntLikeMap VarId (PatF f v VarId)
pgNodes forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall c (g :: * -> *) (f :: * -> *) v.
SolEnv c g f v -> PatGraph g f v
sePatGraph)
      case PatF f v VarId
n of
        -- Free var, choose a solution for each class in `sgByVar i`
        FreePureF v
_ -> do
          IntLikeSet c
cs <- forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks (forall x a. Coercible x Int => x -> IntLikeMap x a -> a
ILM.partialLookup VarId
i forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall c (f :: * -> *).
SolGraph c f -> IntLikeMap VarId (IntLikeSet c)
sgByVar forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall c (g :: * -> *) (f :: * -> *) v.
SolEnv c g f v -> SolGraph c f
seSolGraph)
          forall c (f :: * -> *) v (g :: * -> *).
SolveC c f v =>
VarId -> IntLikeSet c -> SolStream c g f v c
solveChoose VarId
i IntLikeSet c
cs
        -- Embedded functor, traverse and emit solution if present
        FreeEmbedF f VarId
fi -> do
          f c
fa <- forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall c (f :: * -> *) v (g :: * -> *).
SolveC c f v =>
VarId -> SolStream c g f v c
solveRec f VarId
fi
          Maybe c
mc <- forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks (forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
HashMap.lookup f c
fa forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall c (f :: * -> *). SolGraph c f -> HashMap (f c) c
sgNodes forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall c (g :: * -> *) (f :: * -> *) v.
SolEnv c g f v -> SolGraph c f
seSolGraph)
          case Maybe c
mc of
            Maybe c
Nothing -> forall (f :: * -> *) a. Alternative f => f a
empty
            Just c
c -> forall c (g :: * -> *) (f :: * -> *) v.
VarId -> c -> SolStream c g f v c
solveSet VarId
i c
c

-- | The easiest way to do e-matching: given a pattern and an e-graph, yield the list of matches.
-- Note that it's more efficient to keep a 'PatGraph' and use the same solution graph for multiple patterns.)
match :: (PatGraphC f v, SolGraphC f, SolveC EClassId f v) => Pat f v -> EGraph d f -> [MatchSubst EClassId f v]
match :: forall (f :: * -> *) v d.
(PatGraphC f v, SolGraphC f, SolveC EClassId f v) =>
Pat f v -> EGraph d f -> [MatchSubst EClassId f v]
match Pat f v
p EGraph d f
eg =
  let pg :: PatGraph Identity f v
pg = forall (f :: * -> *) v.
PatGraphC f v =>
Pat f v -> PatGraph Identity f v
singlePatGraph Pat f v
p
      sg :: SolGraph EClassId f
sg = forall (f :: * -> *) (g :: * -> *) v d.
SolGraphC f =>
PatGraph g f v -> EGraph d f -> SolGraph EClassId f
solGraph PatGraph Identity f v
pg EGraph d f
eg
  in if forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any forall x. IntLikeSet x -> Bool
ILS.null (forall x a. IntLikeMap x a -> [a]
ILM.elems (forall c (f :: * -> *).
SolGraph c f -> IntLikeMap VarId (IntLikeSet c)
sgByVar SolGraph EClassId f
sg))
    -- If any var id has no patches, the pattern won't match, so don't try to solve
    then []
    else forall r s a. Stream r s a -> r -> s -> [a]
streamAll forall (g :: * -> *) c (f :: * -> *) v.
(Foldable g, SolveC c f v) =>
SolStream c g f v (MatchSubst c f v)
solve (forall c (g :: * -> *) (f :: * -> *) v.
PatGraph g f v -> SolGraph c f -> SolEnv c g f v
SolEnv PatGraph Identity f v
pg SolGraph EClassId f
sg) (forall c. IntLikeMap VarId c -> SolState c
SolState forall x a. IntLikeMap x a
ILM.empty)