-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/


-- | Generic rewriting library for regular datatypes.
--   
--   This package provides rewriting functionality for regular datatypes.
--   Regular datatypes are recursive datatypes such as lists, binary trees,
--   etc. This library cannot be used with mutually recursive datatypes or
--   with nested datatypes.
--   
--   This library has been described in the paper:
--   
--   <ul>
--   <li><i>A Lightweight Approach to Datatype-Generic Rewriting.</i>
--   Thomas van Noort, Alexey Rodriguez, Stefan Holdermans, Johan Jeuring,
--   Bastiaan Heeren. ACM SIGPLAN Workshop on Generic Programming
--   2008.</li>
--   </ul>
--   
--   More information about this library can be found at
--   <a>http://www.cs.uu.nl/wiki/GenericProgramming/Rewriting</a>.
@package rewriting
@version 0.1


-- | Summary: Types for structural representation.
module Generics.Regular.Rewriting.Representations

-- | Structure type for constant values.
data K a r
K :: a -> K a r

-- | Structure type for recursive values.
data Id r
Id :: r -> Id r

-- | Structure type for empty constructors.
data Unit r
Unit :: Unit r

-- | Structure type for alternatives in a type.
data (:+:) f g r
L :: (f r) -> :+: f g r
R :: (g r) -> :+: f g r

-- | Structure type for fields of a constructor.
data (:*:) f g r
(:*:) :: f r -> g r -> :*: f g r

-- | Structure type to store the name of a constructor.
data Con f r
Con :: String -> (f r) -> Con f r

-- | The well-known fixed-point type.
newtype Fix f
In :: (f (Fix f)) -> Fix f

-- | corresponding embedding-projection pairs.
--   
--   The type class <tt>Regular</tt> captures the structural representation
--   of a type and the corresponding embedding-projection pairs.
--   
--   To be able to use the rewriting functions, the user is required to
--   provide an instance of this type class.
class (Functor (PF a)) => Regular a where { type family PF a :: * -> *; }
from :: (Regular a) => a -> PF a a
to :: (Regular a) => PF a a -> a


-- | Summary: Base generic functions that are used for generic rewriting.
module Generics.Regular.Rewriting.Base

-- | The <tt>GMap</tt> class defines a monadic functorial map.
class GMap f
fmapM :: (GMap f, Monad m) => (a -> m b) -> f a -> m (f b)

-- | The <tt>Crush</tt> class defines a crush on functorial values. In
--   fact, <tt>crush</tt> is a generalized <tt>foldr</tt>.
class Crush f
crush :: (Crush f) => (a -> b -> b) -> b -> f a -> b

-- | Flatten a structure by collecting all the elements present.
flatten :: (Crush f) => f a -> [a]

-- | The <tt>Zip</tt> class defines a monadic zip on functorial values.
class Zip f
fzipM :: (Zip f, Monad m) => (a -> b -> m c) -> f a -> f b -> m (f c)

-- | Functorial zip with a non-monadic function, resulting in a monadic
--   value.
fzip :: (Zip f, Monad m) => (a -> b -> c) -> f a -> f b -> m (f c)

-- | Partial functorial zip with a non-monadic function.
fzip' :: (Zip f) => (a -> b -> c) -> f a -> f b -> f c

-- | Equality on values based on their structural representation.
geq :: (b ~ (PF a), Regular a, Crush b, Zip b) => a -> a -> Bool

-- | The <tt>GShow</tt> class defines a show on values.
class GShow f
gshow :: (GShow f) => (a -> ShowS) -> f a -> ShowS

-- | The <tt>LRBase</tt> class defines two functions, <tt>leftb</tt> and
--   <tt>rightb</tt>, which should produce different values.
class LRBase a
leftb :: (LRBase a) => a
rightb :: (LRBase a) => a

-- | The <tt>LR</tt> class defines two functions, <tt>leftf</tt> and
--   <tt>rightf</tt>, which should produce different functorial values.
class LR f
leftf :: (LR f) => a -> f a
rightf :: (LR f) => a -> f a

-- | Produces a value which should be different from the value returned by
--   <tt>right</tt>.
left :: (Regular a, LR (PF a)) => a

-- | Produces a value which should be different from the value returned by
--   <tt>left</tt>.
right :: (Regular a, LR (PF a)) => a
instance (LR f) => LR (Con f)
instance (LR f, LR g) => LR (f :*: g)
instance (LR f, LR g) => LR (f :+: g)
instance LR Unit
instance (LRBase a) => LR (K a)
instance LR Id
instance (LRBase a) => LRBase [a]
instance LRBase Char
instance LRBase Int
instance (GShow f) => GShow (Con f)
instance (GShow f, GShow g) => GShow (f :*: g)
instance (GShow f, GShow g) => GShow (f :+: g)
instance GShow Unit
instance (Show a) => GShow (K a)
instance GShow Id
instance (Zip f) => Zip (Con f)
instance (Zip f, Zip g) => Zip (f :*: g)
instance (Zip f, Zip g) => Zip (f :+: g)
instance Zip Unit
instance (Eq a) => Zip (K a)
instance Zip Id
instance (Crush f) => Crush (Con f)
instance (Crush f, Crush g) => Crush (f :*: g)
instance (Crush f, Crush g) => Crush (f :+: g)
instance Crush Unit
instance Crush (K a)
instance Crush Id
instance (GMap f) => GMap (Con f)
instance (GMap f, GMap g) => GMap (f :*: g)
instance (GMap f, GMap g) => GMap (f :+: g)
instance GMap Unit
instance GMap (K a)
instance GMap Id
instance (Functor f) => Functor (Con f)
instance (Functor f, Functor g) => Functor (f :*: g)
instance (Functor f, Functor g) => Functor (f :+: g)
instance Functor Unit
instance Functor (K a)
instance Functor Id


-- | Summary: Functions for transforming a rule specification to a rule.
module Generics.Regular.Rewriting.Rules

-- | Specifies a rule as a value of a datatype.
data RuleSpec a
(:~>) :: a -> a -> RuleSpec a

-- | Returns the left-hand side of a rule.
lhsR :: RuleSpec a -> a

-- | Returns the right-hand side of a rule.
rhsR :: RuleSpec a -> a

-- | Allows metavariables on either side of a rule.
type Rule a = RuleSpec (SchemeOf a)

-- | Extends the pattern functor of a value.
type SchemeOf a = Scheme (PF a)
type Metavar = Int

-- | Constructs a metavariable.
metavar :: Metavar -> Scheme f

-- | Constructs a pattern functor value.
pf :: f (Scheme f) -> Scheme f

-- | Recursively converts a value to a <tt>SchemeOf</tt> value.
toScheme :: (Regular a) => a -> SchemeOf a

-- | A view on schemes to easily distinguish metavariables from pattern
--   functor values.
data SchemeView f
Metavar :: Metavar -> SchemeView f
PF :: (f (Scheme f)) -> SchemeView f

-- | Returns the value corresponding to the <tt>SchemeView</tt>.
schemeView :: Scheme f -> SchemeView f

-- | Folds a <tt>Scheme</tt> value given a function to apply to
--   metavariables and a function to apply to a pattern functor value.
foldScheme :: (Functor f) => (Metavar -> a) -> (f a -> a) -> Scheme f -> a

-- | The type class <tt>Builder</tt> captures the functions, that are
--   defined by induction on the type argument, that construct appropriate
--   <tt>left</tt> and <tt>right</tt> values. These values are used to
--   transform a rule specification to a rule.
class (Regular (Target a)) => Builder a where { type family Target a :: *; }
base :: (Builder a) => a -> RuleSpec (Target a)
diag :: (Builder a) => a -> [RuleSpec (Target a)]

-- | Transforms a rule specification to a rule and returns <tt>Nothing</tt>
--   if an unbound metavariable occurs in the right-hand side of the rule.
ruleM :: (Builder r, Crush (PF (Target r)), Zip (PF (Target r))) => r -> Maybe (Rule (Target r))

-- | Transforms a rule specification to a rule and throws a runtime error
--   if an unbound metavariable occurs in the right-hand side of the rule.
rule :: (Builder r, Crush (PF (Target r)), Zip (PF (Target r))) => r -> Rule (Target r)
instance (Builder a, Regular b, LR (PF b)) => Builder (b -> a)
instance (Regular a) => Builder (RuleSpec a)


-- | Summary: Core machinery for rewriting terms.
module Generics.Regular.Rewriting.Machinery

-- | The <tt>Rewrite</tt> is a type class synonym, hiding some of the
--   implementation details.
--   
--   To be able to use the rewriting functions, the user is required to
--   provide an instance of this type class.
class (Regular a, Crush (PF a), GMap (PF a), GShow (PF a), Zip (PF a), LR (PF a)) => Rewrite a

-- | Applies a rule specification to a term, obtaining a monadic value.
applyRuleM :: (Builder r, Rewrite (Target r), Monad m) => r -> Target r -> m (Target r)

-- | Applies a rule specification to a term, obtaining the original term
--   when rewriting fails.
applyRule :: (Builder r, Rewrite (Target r)) => r -> Target r -> Target r

-- | Rewrites a term, obtaining a monadic value.
rewriteM :: (Rewrite a, Monad m) => Rule a -> a -> m a

-- | Rewrites a term, obtaining the original term when rewriting fails.
rewrite :: (Rewrite a) => Rule a -> a -> a


-- | Summary: Generic functions for traversal strategies.
module Generics.Regular.Rewriting.Strategies

-- | Applies a function to the first subtree (possibly the tree itself) on
--   which it succeeds, using a preorder traversal.
once :: (Regular a, GMap (PF a), Functor m, MonadPlus m) => (a -> m a) -> a -> m a

-- | Applies a function to the first immediate child of a value on which it
--   succeeds.
one :: (Regular a, GMap (PF a), Functor m, MonadPlus m) => (a -> m a) -> a -> m a

-- | Applies a monadic function exhaustively in a top-down fashion.
topdownM :: (Regular a, GMap (PF a), Functor m, Monad m) => (a -> m a) -> a -> m a

-- | Applies a function exhaustively in a top-down fashion
topdown :: (Regular a) => (a -> a) -> a -> a

-- | Applies a monadic function exhaustively in a bottom-up fashion.
bottomupM :: (Regular a, GMap (PF a), Functor m, Monad m) => (a -> m a) -> a -> m a

-- | Applies a function exhaustively in a bottom-up fashion
bottomup :: (Regular a) => (a -> a) -> a -> a

-- | Applies a monadic function to all the immediate children of a value.
composM :: (Regular a, GMap (PF a), Functor m, Monad m) => (a -> m a) -> a -> m a

-- | Applies a function to all the immediate children of a value.
compos :: (Regular a) => (a -> a) -> a -> a
instance (MonadPlus m) => Monad (S m)


-- | By importing this module, the user is able to use all the rewriting
--   machinery. The user is only required to provide an instance of
--   <tt>Regular</tt> and <tt>Rewrite</tt> for his datatype.
--   
--   Consider a datatype representing logical propositions:
--   
--   <pre>
--   data Expr = Const Int | Expr :++: Expr | Expr :**: Expr deriving Show
--   </pre>
--   
--   An instance of <tt>Regular</tt> would look like:
--   
--   <pre>
--   instance Regular Expr where
--     type PF Expr = K Int :+: Id :*: Id :+: Id :*: Id
--     from (Const n)    = L (K n)
--     from (e1 :++: e2) = R (L  $ (Id e1) :*: (Id e2))
--     from (e1 :**: e2) = R (R  $ (Id e1) :*: (Id e2))
--     to (L (K n))                     = Const n
--     to (R (L ((Id r1) :*: (Id r2)))) = r1 :++: r2
--     to (R (R ((Id r1) :*: (Id r2)))) = r1 :**: r2
--   </pre>
--   
--   Additionally, the instance <tt>Rewrite</tt> would look like:
--   
--   <pre>
--   instance Rewrite Expr
--   </pre>
--   
--   Build rules like this:
--   
--   <pre>
--   rule1 :: Rule Expr
--   rule1 = 
--     rule $ x -&gt; x :++: Const 0 :~&gt;
--                 x
--   rule5 :: Rule Expr
--   rule5 = 
--     rule $ x y z -&gt; x :**: (y :++: z) :~&gt;  
--                     (x :**: y) :++: (x :**: z) 
--   </pre>
--   
--   And apply them as follows:
--   
--   <pre>
--   test1 :: Maybe Expr
--   test1 = rewriteM rule1 (Const 2 :++: Const 0)
--   test10 :: Maybe Expr
--   test10 = rewriteM rule5 ((Const 1) :**: ((Const 2) :++: (Const 3)))
--   </pre>
--   
--   You may also wish to add constructor names in the representation to
--   use generic show. However, constructor names are not yet a stable
--   feature and will probably change in future versions of this library.
--   
--   <pre>
--   instance Regular Expr where
--     type PF Expr = Con (K Int) :+: Con (Id :*: Id) :+: Con (Id :*: Id)
--     from (Const n)    = L (Con "Const" (K n))
--     from (e1 :++: e2) = R (L (Con "(:++:)" $ (Id e1) :*: (Id e2)))
--     from (e1 :**: e2) = R (R (Con "(:**:)" $ (Id e1) :*: (Id e2)))
--     to (L (Con _ (K n)))                        = Const n
--     to (R (L (Con _ ((Id r1) :*: (Id r2))))) = r1 :++: r2
--     to (R (R (Con _ ((Id r1) :*: (Id r2))))) = r1 :**: r2
--   </pre>
module Generics.Regular.Rewriting