{-# LANGUAGE GADTs #-}
{-# LANGUAGE Rank2Types #-}
module Data.Comp.TermRewriting where
import Prelude hiding (any)
import Data.Comp.Algebra
import Data.Comp.Equality
import Data.Comp.Matching
import Data.Comp.Sum
import Data.Comp.Term
import Data.Foldable
import Data.Map (Map)
import qualified Data.Map as Map
import Data.Maybe
import qualified Data.Set as Set
import Control.Monad
type RPS f g = Hom f g
type Var = Int
type Rule f g v = (Context f v, Context g v)
type TRS f g v = [Rule f g v]
type Step t = t -> Maybe t
type BStep t = t -> (t,Bool)
matchRule :: (Ord v, EqF f, Eq a, Functor f, Foldable f)
=> Rule f g v -> Cxt h f a -> Maybe (Context g v, Map v (Cxt h f a))
matchRule :: Rule f g v -> Cxt h f a -> Maybe (Context g v, Map v (Cxt h f a))
matchRule (Context f v
lhs,Context g v
rhs) Cxt h f a
t = do
Map v (Cxt h f a)
subst <- Context f v -> Cxt h f a -> Maybe (Map v (Cxt h f a))
forall v (f :: * -> *) h a.
(Ord v, EqF f, Eq (Cxt h f a), Functor f, Foldable f) =>
Context f v -> Cxt h f a -> Maybe (CxtSubst h a f v)
matchCxt Context f v
lhs Cxt h f a
t
(Context g v, Map v (Cxt h f a))
-> Maybe (Context g v, Map v (Cxt h f a))
forall (m :: * -> *) a. Monad m => a -> m a
return (Context g v
rhs,Map v (Cxt h f a)
subst)
matchRules :: (Ord v, EqF f, Eq a, Functor f, Foldable f)
=> TRS f g v -> Cxt h f a -> Maybe (Context g v, Map v (Cxt h f a))
matchRules :: TRS f g v -> Cxt h f a -> Maybe (Context g v, Map v (Cxt h f a))
matchRules TRS f g v
trs Cxt h f a
t = [(Context g v, Map v (Cxt h f a))]
-> Maybe (Context g v, Map v (Cxt h f a))
forall a. [a] -> Maybe a
listToMaybe ([(Context g v, Map v (Cxt h f a))]
-> Maybe (Context g v, Map v (Cxt h f a)))
-> [(Context g v, Map v (Cxt h f a))]
-> Maybe (Context g v, Map v (Cxt h f a))
forall a b. (a -> b) -> a -> b
$ (Rule f g v -> Maybe (Context g v, Map v (Cxt h f a)))
-> TRS f g v -> [(Context g v, Map v (Cxt h f a))]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (Rule f g v -> Cxt h f a -> Maybe (Context g v, Map v (Cxt h f a))
forall v (f :: * -> *) a (g :: * -> *) h.
(Ord v, EqF f, Eq a, Functor f, Foldable f) =>
Rule f g v -> Cxt h f a -> Maybe (Context g v, Map v (Cxt h f a))
`matchRule` Cxt h f a
t) TRS f g v
trs
appRule :: (Ord v, EqF f, Eq a, Functor f, Foldable f)
=> Rule f f v -> Step (Cxt h f a)
appRule :: Rule f f v -> Step (Cxt h f a)
appRule Rule f f v
rule Cxt h f a
t = do
(Context f v
res, Map v (Cxt h f a)
subst) <- Rule f f v -> Cxt h f a -> Maybe (Context f v, Map v (Cxt h f a))
forall v (f :: * -> *) a (g :: * -> *) h.
(Ord v, EqF f, Eq a, Functor f, Foldable f) =>
Rule f g v -> Cxt h f a -> Maybe (Context g v, Map v (Cxt h f a))
matchRule Rule f f v
rule Cxt h f a
t
Step (Cxt h f a)
forall (m :: * -> *) a. Monad m => a -> m a
return Step (Cxt h f a) -> Step (Cxt h f a)
forall a b. (a -> b) -> a -> b
$ Context f v -> Map v (Cxt h f a) -> Cxt h f a
forall (f :: * -> *) (g :: * -> *) v h' h a.
(Functor f, Functor g, f :<: g, Ord v) =>
Cxt h' f v -> Map v (Cxt h g a) -> Cxt h g a
substHoles' Context f v
res Map v (Cxt h f a)
subst
appTRS :: (Ord v, EqF f, Eq a, Functor f, Foldable f)
=> TRS f f v -> Step (Cxt h f a)
appTRS :: TRS f f v -> Step (Cxt h f a)
appTRS TRS f f v
trs Cxt h f a
t = [Cxt h f a] -> Maybe (Cxt h f a)
forall a. [a] -> Maybe a
listToMaybe ([Cxt h f a] -> Maybe (Cxt h f a))
-> [Cxt h f a] -> Maybe (Cxt h f a)
forall a b. (a -> b) -> a -> b
$ (Rule f f v -> Maybe (Cxt h f a)) -> TRS f f v -> [Cxt h f a]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (Rule f f v -> Step (Cxt h f a)
forall v (f :: * -> *) a h.
(Ord v, EqF f, Eq a, Functor f, Foldable f) =>
Rule f f v -> Step (Cxt h f a)
`appRule` Cxt h f a
t) TRS f f v
trs
bStep :: Step t -> BStep t
bStep :: Step t -> BStep t
bStep Step t
f t
t = case Step t
f t
t of
Maybe t
Nothing -> (t
t, Bool
False)
Just t
t' -> (t
t',Bool
True)
parTopStep :: (Ord v, EqF f, Eq a, Foldable f, Functor f)
=> TRS f f v -> Step (Cxt h f a)
parTopStep :: TRS f f v -> Step (Cxt h f a)
parTopStep TRS f f v
_ Hole{} = Maybe (Cxt h f a)
forall a. Maybe a
Nothing
parTopStep TRS f f v
trs c :: Cxt h f a
c@(Term f (Cxt h f a)
t) = Maybe (Cxt h f a)
tTop Maybe (Cxt h f a) -> Maybe (Cxt h f a) -> Maybe (Cxt h f a)
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
`mplus` Maybe (Cxt h f a)
tBelow'
where tTop :: Maybe (Cxt h f a)
tTop = TRS f f v -> Step (Cxt h f a)
forall v (f :: * -> *) a h.
(Ord v, EqF f, Eq a, Functor f, Foldable f) =>
TRS f f v -> Step (Cxt h f a)
appTRS TRS f f v
trs Cxt h f a
c
tBelow :: f (Cxt h f a, Bool)
tBelow = (Cxt h f a -> (Cxt h f a, Bool))
-> f (Cxt h f a) -> f (Cxt h f a, Bool)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Step (Cxt h f a) -> Cxt h f a -> (Cxt h f a, Bool)
forall t. Step t -> BStep t
bStep (Step (Cxt h f a) -> Cxt h f a -> (Cxt h f a, Bool))
-> Step (Cxt h f a) -> Cxt h f a -> (Cxt h f a, Bool)
forall a b. (a -> b) -> a -> b
$ TRS f f v -> Step (Cxt h f a)
forall v (f :: * -> *) a h.
(Ord v, EqF f, Eq a, Foldable f, Functor f) =>
TRS f f v -> Step (Cxt h f a)
parTopStep TRS f f v
trs) f (Cxt h f a)
t
tAny :: Bool
tAny = ((Cxt h f a, Bool) -> Bool) -> f (Cxt h f a, Bool) -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Cxt h f a, Bool) -> Bool
forall a b. (a, b) -> b
snd f (Cxt h f a, Bool)
tBelow
tBelow' :: Maybe (Cxt h f a)
tBelow'
| Bool
tAny = Step (Cxt h f a)
forall a. a -> Maybe a
Just Step (Cxt h f a) -> Step (Cxt h f a)
forall a b. (a -> b) -> a -> b
$ f (Cxt h f a) -> Cxt h f a
forall (f :: * -> *) h a. f (Cxt h f a) -> Cxt h f a
Term (f (Cxt h f a) -> Cxt h f a) -> f (Cxt h f a) -> Cxt h f a
forall a b. (a -> b) -> a -> b
$ ((Cxt h f a, Bool) -> Cxt h f a)
-> f (Cxt h f a, Bool) -> f (Cxt h f a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Cxt h f a, Bool) -> Cxt h f a
forall a b. (a, b) -> a
fst f (Cxt h f a, Bool)
tBelow
| Bool
otherwise = Maybe (Cxt h f a)
forall a. Maybe a
Nothing
parallelStep :: (Ord v, EqF f, Eq a,Foldable f, Functor f)
=> TRS f f v -> Step (Cxt h f a)
parallelStep :: TRS f f v -> Step (Cxt h f a)
parallelStep TRS f f v
_ Hole{} = Maybe (Cxt h f a)
forall a. Maybe a
Nothing
parallelStep TRS f f v
trs c :: Cxt h f a
c@(Term f (Cxt h f a)
t) =
case TRS f f v -> Cxt h f a -> Maybe (Context f v, Map v (Cxt h f a))
forall v (f :: * -> *) a (g :: * -> *) h.
(Ord v, EqF f, Eq a, Functor f, Foldable f) =>
TRS f g v -> Cxt h f a -> Maybe (Context g v, Map v (Cxt h f a))
matchRules TRS f f v
trs Cxt h f a
c of
Maybe (Context f v, Map v (Cxt h f a))
Nothing
| Bool
anyBelow -> Step (Cxt h f a)
forall a. a -> Maybe a
Just Step (Cxt h f a) -> Step (Cxt h f a)
forall a b. (a -> b) -> a -> b
$ f (Cxt h f a) -> Cxt h f a
forall (f :: * -> *) h a. f (Cxt h f a) -> Cxt h f a
Term (f (Cxt h f a) -> Cxt h f a) -> f (Cxt h f a) -> Cxt h f a
forall a b. (a -> b) -> a -> b
$ ((Cxt h f a, Bool) -> Cxt h f a)
-> f (Cxt h f a, Bool) -> f (Cxt h f a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Cxt h f a, Bool) -> Cxt h f a
forall a b. (a, b) -> a
fst f (Cxt h f a, Bool)
below
| Bool
otherwise -> Maybe (Cxt h f a)
forall a. Maybe a
Nothing
where below :: f (Cxt h f a, Bool)
below = (Cxt h f a -> (Cxt h f a, Bool))
-> f (Cxt h f a) -> f (Cxt h f a, Bool)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Step (Cxt h f a) -> Cxt h f a -> (Cxt h f a, Bool)
forall t. Step t -> BStep t
bStep (Step (Cxt h f a) -> Cxt h f a -> (Cxt h f a, Bool))
-> Step (Cxt h f a) -> Cxt h f a -> (Cxt h f a, Bool)
forall a b. (a -> b) -> a -> b
$ TRS f f v -> Step (Cxt h f a)
forall v (f :: * -> *) a h.
(Ord v, EqF f, Eq a, Foldable f, Functor f) =>
TRS f f v -> Step (Cxt h f a)
parallelStep TRS f f v
trs) f (Cxt h f a)
t
anyBelow :: Bool
anyBelow = ((Cxt h f a, Bool) -> Bool) -> f (Cxt h f a, Bool) -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Cxt h f a, Bool) -> Bool
forall a b. (a, b) -> b
snd f (Cxt h f a, Bool)
below
Just (Context f v
rhs,Map v (Cxt h f a)
subst) -> Step (Cxt h f a)
forall a. a -> Maybe a
Just Step (Cxt h f a) -> Step (Cxt h f a)
forall a b. (a -> b) -> a -> b
$ Context f v -> Map v (Cxt h f a) -> Cxt h f a
forall (f :: * -> *) (g :: * -> *) v h' h a.
(Functor f, Functor g, f :<: g, Ord v) =>
Cxt h' f v -> Map v (Cxt h g a) -> Cxt h g a
substHoles' Context f v
rhs Map v (Cxt h f a)
substBelow
where rhsVars :: Set v
rhsVars = [v] -> Set v
forall a. Ord a => [a] -> Set a
Set.fromList ([v] -> Set v) -> [v] -> Set v
forall a b. (a -> b) -> a -> b
$ Context f v -> [v]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList Context f v
rhs
substBelow :: Map v (Cxt h f a)
substBelow = (v -> Step (Cxt h f a)) -> Map v (Cxt h f a) -> Map v (Cxt h f a)
forall k a b. (k -> a -> Maybe b) -> Map k a -> Map k b
Map.mapMaybeWithKey v -> Step (Cxt h f a)
apply Map v (Cxt h f a)
subst
apply :: v -> Step (Cxt h f a)
apply v
v Cxt h f a
t
| v -> Set v -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member v
v Set v
rhsVars = Step (Cxt h f a)
forall a. a -> Maybe a
Just Step (Cxt h f a) -> Step (Cxt h f a)
forall a b. (a -> b) -> a -> b
$ (Cxt h f a, Bool) -> Cxt h f a
forall a b. (a, b) -> a
fst ((Cxt h f a, Bool) -> Cxt h f a) -> (Cxt h f a, Bool) -> Cxt h f a
forall a b. (a -> b) -> a -> b
$ Step (Cxt h f a) -> Cxt h f a -> (Cxt h f a, Bool)
forall t. Step t -> BStep t
bStep (TRS f f v -> Step (Cxt h f a)
forall v (f :: * -> *) a h.
(Ord v, EqF f, Eq a, Foldable f, Functor f) =>
TRS f f v -> Step (Cxt h f a)
parallelStep TRS f f v
trs) Cxt h f a
t
| Bool
otherwise = Maybe (Cxt h f a)
forall a. Maybe a
Nothing
reduce :: Step t -> t -> t
reduce :: Step t -> t -> t
reduce Step t
s t
t = case Step t
s t
t of
Maybe t
Nothing -> t
t
Just t
t' -> Step t -> t -> t
forall t. Step t -> t -> t
reduce Step t
s t
t'