{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE UndecidableInstances #-}
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 (..))
type Pat = Free
type PatF = FreeF
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
type PatGroup g f v = g (Pat f v)
type Subst c v = HashMap v c
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
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)
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)
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)
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
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
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
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)
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)
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)
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
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
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
data SolGraph c f = SolGraph
{ forall c (f :: * -> *).
SolGraph c f -> IntLikeMap VarId (IntLikeSet c)
sgByVar :: !(IntLikeMap VarId (IntLikeSet c))
, forall c (f :: * -> *). SolGraph c f -> HashMap (f c) c
sgNodes :: !(HashMap (f c) c)
}
deriving stock instance (Eq c, Eq (f c)) => Eq (SolGraph c f)
deriving stock instance (Show c, Show (f c)) => Show (SolGraph c f)
type SolGraphC f = (Functor f, Foldable f, Eq (f ()), Hashable (f ()))
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 =
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
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
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)
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)
type SolStream c g f v z = Stream (SolEnv c g f v) (SolState c) z
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
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
Just c
s -> forall (f :: * -> *) a. Applicative f => a -> f a
pure c
s
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
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
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
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))
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)