{-# LANGUAGE GADTs      #-}
{-# LANGUAGE Rank2Types #-}
--------------------------------------------------------------------------------
-- |
-- Module      :  Data.Comp.TermRewriting
-- Copyright   :  (c) 2010-2011 Patrick Bahr
-- License     :  BSD3
-- Maintainer  :  Patrick Bahr <paba@diku.dk>
-- Stability   :  experimental
-- Portability :  non-portable (GHC Extensions)
--
-- This module defines term rewriting systems (TRSs) using compositional data
-- types.
--
--------------------------------------------------------------------------------

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


{-| This type represents /recursive program schemes/.  -}

type RPS f g  = Hom f g

-- | This type represents variables.
type Var = Int

{-| This type represents term rewrite rules from signature @f@ to
signature @g@ over variables of type @v@ -}

type Rule f g v = (Context f v, Context g v)


{-| This type represents term rewriting systems (TRSs) from signature
@f@ to signature @g@ over variables of type @v@. -}

type TRS f g v = [Rule f g v]

-- | This type represents a potential single step reduction from any
-- input.
type Step t = t -> Maybe t

-- | This type represents a potential single step reduction from any
-- input. If there is no single step then the return value is the
-- input together with @False@. Otherwise, the successor is returned
-- together with @True@.
type BStep t = t -> (t,Bool)

{-| This function tries to match the given rule against the given term
(resp. context in general) at the root. If successful, the function
returns the right hand side of the rule and the matching
substitution. -}

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 :: 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 (Context f v
lhs,Context g v
rhs) Cxt h f a
t = do
  Map v (Cxt h f a)
subst <- 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
  forall (m :: * -> *) a. Monad m => a -> m a
return (Context g v
rhs,Map v (Cxt h f a)
subst)

-- | This function tries to match the rules of the given TRS against
-- the given term (resp. context in general) at the root. The first
-- rule in the TRS that matches is then used and the corresponding
-- right-hand side as well the matching substitution is returned.
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 :: 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 g v
trs Cxt h f a
t = forall a. [a] -> Maybe a
listToMaybe forall a b. (a -> b) -> a -> b
$ forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (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

{-| This function tries to apply the given rule at the root of the
given term (resp. context in general). If successful, the function
returns the result term of the rewrite step; otherwise @Nothing@. -}

appRule :: (Ord v, EqF f, Eq a, Functor f, Foldable f)
          => Rule f f v -> Step (Cxt h f a)
appRule :: 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 Rule f f v
rule Cxt h f a
t = do
  (Context f v
res, Map v (Cxt h f a)
subst) <- 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
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ 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

{-| This function tries to apply one of the rules in the given TRS at
the root of the given term (resp. context in general) by trying each
rule one by one using 'appRule' until one rule is applicable. If no
rule is applicable @Nothing@ is returned. -}

appTRS :: (Ord v, EqF f, Eq a, Functor f, Foldable f)
         => TRS f f v -> Step (Cxt h f a)
appTRS :: 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
t = forall a. [a] -> Maybe a
listToMaybe forall a b. (a -> b) -> a -> b
$ forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (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


{-| This is an auxiliary function that turns function @f@ of type
  @(t -> Maybe t)@ into functions @f'@ of type @t -> (t,Bool)@. @f' x@
  evaluates to @(y,True)@ if @f x@ evaluates to @Just y@, and to
  @(x,False)@ if @f x@ evaluates to @Nothing@. This function is useful
  to change the output of functions that apply rules such as 'appTRS'. -}

bStep :: Step t -> BStep t
bStep :: forall t. 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)

{-| This function performs a parallel reduction step by trying to
apply rules of the given system to all outermost redexes. If the given
term contains no redexes, @Nothing@ is returned. -}

parTopStep :: (Ord v, EqF f, Eq a, Foldable f, Functor f)
           => TRS f f v -> Step (Cxt h f a)
parTopStep :: 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
_ Hole{} = 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 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 = 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 = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall t. Step t -> BStep t
bStep forall a b. (a -> b) -> a -> b
$ 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 = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any forall a b. (a, b) -> b
snd f (Cxt h f a, Bool)
tBelow
          tBelow' :: Maybe (Cxt h f a)
tBelow'
              | Bool
tAny = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall (b :: * -> *) a c. b (Cxt a b c) -> Cxt a b c
Term forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. (a, b) -> a
fst f (Cxt h f a, Bool)
tBelow
              | Bool
otherwise = forall a. Maybe a
Nothing

{-| This function performs a parallel reduction step by trying to
apply rules of the given system to all outermost redexes and then
recursively in the variable positions of the redexes. If the given
term does not contain any redexes, @Nothing@ is returned. -}

parallelStep :: (Ord v, EqF f, Eq a,Foldable f, Functor  f)
             => TRS f f v -> Step (Cxt h f a)
parallelStep :: 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
_ Hole{} = 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 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 -> forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall (b :: * -> *) a c. b (Cxt a b c) -> Cxt a b c
Term forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. (a, b) -> a
fst f (Cxt h f a, Bool)
below
          | Bool
otherwise -> forall a. Maybe a
Nothing
        where below :: f (Cxt h f a, Bool)
below = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall t. Step t -> BStep t
bStep forall a b. (a -> b) -> a -> b
$ 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 = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any 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) -> forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ 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 = forall a. Ord a => [a] -> Set a
Set.fromList forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t a -> [a]
toList Context f v
rhs
                substBelow :: Map v (Cxt h f a)
substBelow = forall k a b. (k -> a -> Maybe b) -> Map k a -> Map k b
Map.mapMaybeWithKey v -> Cxt h f a -> Maybe (Cxt h f a)
apply Map v (Cxt h f a)
subst
                apply :: v -> Cxt h f a -> Maybe (Cxt h f a)
apply v
v Cxt h f a
t
                    | forall a. Ord a => a -> Set a -> Bool
Set.member v
v Set v
rhsVars = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a b. (a, b) -> a
fst forall a b. (a -> b) -> a -> b
$ forall t. Step t -> BStep t
bStep (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 = forall a. Maybe a
Nothing


{-| This function applies the given reduction step repeatedly until a
normal form is reached. -}

reduce :: Step t -> t -> t
reduce :: forall t. 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' -> forall t. Step t -> t -> t
reduce Step t
s t
t'