compstrat
CopyrightJames Koppel 2013
LicenseBSD-style (see the LICENSE file in the distribution)
Safe HaskellNone
LanguageHaskell2010

Data.Comp.Multi.Strategic

Description

Strategy combinators for cubix-compdata. Older versions of this package were built for vanilla compdata.

Strategy combinators are functions that build more complicated traversals out of smaller (perhaps single-node) traversals. The name comes from the idea of a rewriting strategy, an algorithm for choosing how to apply a set of rewrite rules. For a tutorial introduction to strategy combinators, see:

Functions in this module have a particular naming schema:

  • Suffix R (e.g.: anybuR): Short for "rewrite". It means the function is type-preserving (rewrites a term to another term of the same sort).
  • Suffix T (e.g.: onetdT): Short for "translate". It means the function rewrites a tree to a fixed type.
  • Suffix F (e.g.: promoteTF): Short for "failable". This denotes combinators whose result is a rewrite in the Maybe monad.
  • td (e.g.: crushtdT): Short for "top-down traversal"
  • bu (e.g.: anybuR): Short for "bottom-up traversal"

The design (and naming system) of compstrat is heavily inspired by an older library of strategy combinators, KURE, https://hackage.haskell.org/package/kure

Synopsis

Rewrites

Core types

type RewriteM (m :: Type -> Type) (f :: Type -> Type) l = f l -> m (f l) Source #

The basic type of rewrites. A RewriteM m f l rewrites a term of signature f, sort l, to another such term, with effects in monad m

Rewrite m f l is equivalent to TranslateM m f l (f l).

type Rewrite (f :: Type -> Type) l = RewriteM Identity f l Source #

A rewrite with no effects

type GRewriteM (m :: Type -> Type) (f :: Type -> Type) = forall l. RewriteM m f l Source #

An effectful rewrite that runs on terms of any sort

type GRewrite (f :: Type -> Type) = GRewriteM Identity f Source #

A rewrite that runs on terms of any sort and has no effects

Rewrite combinators for failure

addFail :: Monad m => TranslateM m f l t -> TranslateM (MaybeT m) f l t Source #

Lifts a translation into the Maybe monad, allowing it to fail

tryR :: Monad m => RewriteM (MaybeT m) f l -> RewriteM m f l Source #

Turns a rewrite that may fail into one that unconditionally succeeds, replacing failures with identity.

failR :: MonadPlus m => RewriteM m f l Source #

The rewrite that always fails

Rewrite combinators for sorts

dynamicR :: (DynCase f l, MonadPlus m) => RewriteM m f l -> GRewriteM m f Source #

Turns a rewrite that runs on a single sort to one that runs on any sort, failing for all other sorts.

promoteR :: forall f l (m :: Type -> Type). (DynCase f l, Monad m) => RewriteM (MaybeT m) f l -> GRewriteM m f Source #

Turns a failable rewrite on one sort l into a rewrite that always succeeds, and runs on any sort, performing the identity rewrite on terms of sort other than l. Defined tryR . dynamicR

promoteRF :: forall f l (m :: Type -> Type). (DynCase f l, Monad m) => RewriteM (MaybeT m) f l -> GRewriteM (MaybeT m) f Source #

Turns a rewrite that runs on a single sort to one that runs on any sort, failing for all other sorts. Equivalent to dynamicR

Sequential combination of rewrites

(>+>) :: forall (m :: Type -> Type) (f :: Type -> Type). MonadPlus m => GRewriteM m f -> GRewriteM m f -> GRewriteM m f Source #

Applies two rewrites in suceesion, succeeding if one or both succeed

(<+) :: Alternative m => TranslateM m f l t -> TranslateM m f l t -> TranslateM m f l t Source #

Left-biased choice -- (f <+ g) runs f, and, if it fails, then runs g

One-level traversal combinators

allR :: forall m (f :: (Type -> Type) -> Type -> Type) h (a :: Type -> Type) l. (Applicative m, HTraversable f) => GRewriteM m (Cxt h f a) -> RewriteM m (Cxt h f a) l Source #

Applies a rewrite to all immediate subterms of the current term. Ignores holes.

revAllR :: forall m (f :: (Type -> Type) -> Type -> Type) h (a :: Type -> Type) l. (Applicative m, HTraversable f) => GRewriteM m (Cxt h f a) -> RewriteM m (Cxt h f a) l Source #

Like allR, but runs on the children in reverse order

anyR :: forall m (f :: (Type -> Type) -> Type -> Type) h (a :: Type -> Type) l. (MonadPlus m, HTraversable f) => GRewriteM m (Cxt h f a) -> RewriteM m (Cxt h f a) l Source #

Applies a rewrite to all immediate subterms of the current term, succeeding if any succeed Ignores holes.

oneR :: forall m (f :: (Type -> Type) -> Type -> Type) h (a :: Type -> Type) l. (MonadPlus m, HTraversable f) => GRewriteM m (Cxt h f a) -> RewriteM m (Cxt h f a) l Source #

Applies a rewrite to the first immediate subterm of the current term where it can succeed Ignores holes.

allStateR Source #

Arguments

:: forall m (f :: (Type -> Type) -> Type -> Type) s h (a :: Type -> Type) l. (Monad m, HTraversable f) 
=> (forall i. s -> Cxt h f a i -> m (Cxt h f a i, s))

A stateful computation

-> s

The start state

-> RewriteM m (Cxt h f a) l 

Runs a stateful computation on all immediate children of the current term.

allIdxR :: forall m (f :: (Type -> Type) -> Type -> Type) h (a :: Type -> Type) l. (Monad m, HTraversable f) => (Int -> GRewriteM m (Cxt h f a)) -> RewriteM m (Cxt h f a) l Source #

Let f be a rewrite with an extra Int parameter, intended to be called f i t, where t is a term and i is the index of t among its parent's children. Then allIdxR f x runs f on all children of x.

Whole-term traversals

alltdR :: forall (m :: Type -> Type) (f :: (Type -> Type) -> Type -> Type) h (a :: Type -> Type). (Monad m, HTraversable f) => GRewriteM m (Cxt h f a) -> GRewriteM m (Cxt h f a) Source #

Runs a rewrite in a top-down traversal Defined: alltdR f = f >=> allR (alltdR f)

Ignores holes.

allbuR :: forall (m :: Type -> Type) (f :: (Type -> Type) -> Type -> Type) h (a :: Type -> Type). (Monad m, HTraversable f) => GRewriteM m (Cxt h f a) -> GRewriteM m (Cxt h f a) Source #

Runs a rewrite in a bottom-up traversal. Defined: allbuR f = allR (allbuR f) >=> f Ignores holes.

anytdR :: forall (m :: Type -> Type) (f :: (Type -> Type) -> Type -> Type) h (a :: Type -> Type). (MonadPlus m, HTraversable f) => GRewriteM m (Cxt h f a) -> GRewriteM m (Cxt h f a) Source #

Runs a rewrite in a top-down traversal, succeeding if any succeed. Defined: anytdR f = f >+> anyR (anytdR f)

anybuR :: forall (m :: Type -> Type) (f :: (Type -> Type) -> Type -> Type) h (a :: Type -> Type). (MonadPlus m, HTraversable f) => GRewriteM m (Cxt h f a) -> GRewriteM m (Cxt h f a) Source #

Runs a rewrite in a bottom-up traversal, succeeding if any succeed. Defined: anybuR f = anyR (anybuR f) >+> f

Ignores holes.

revAllbuR :: forall (m :: Type -> Type) (f :: (Type -> Type) -> Type -> Type) h (a :: Type -> Type). (Monad m, HTraversable f) => GRewriteM m (Cxt h f a) -> GRewriteM m (Cxt h f a) Source #

Like allbuR, but runs in right-to-left order

prunetdRF :: forall (m :: Type -> Type) (f :: (Type -> Type) -> Type -> Type) h (a :: Type -> Type). (MonadPlus m, HTraversable f) => GRewriteM m (Cxt h f a) -> GRewriteM m (Cxt h f a) Source #

Runs a rewrite in a top-down traversal, succeeding if any succeed, and pruning below successes. Defined: prunetdRF f = f <+ anyR (prunetdRF f)

Ignores holes.

prunetdR :: forall (m :: Type -> Type) (f :: (Type -> Type) -> Type -> Type) h (a :: Type -> Type). (Monad m, HTraversable f) => GRewriteM (MaybeT m) (Cxt h f a) -> GRewriteM m (Cxt h f a) Source #

Like prunetdRF, but the outer level always succeeds. Defined tryR . prunetdRF Ignores holes.

onetdR :: forall (m :: Type -> Type) (f :: (Type -> Type) -> Type -> Type) h (a :: Type -> Type). (MonadPlus m, HTraversable f) => GRewriteM m (Cxt h f a) -> GRewriteM m (Cxt h f a) Source #

Applies a rewrite to the first node where it can succeed in a top-down traversal. Defined: onetdR f = f <+ oneR (onetdR f)

Ignores holes.

onebuR :: forall (m :: Type -> Type) (f :: (Type -> Type) -> Type -> Type) h (a :: Type -> Type). (MonadPlus m, HTraversable f) => GRewriteM m (Cxt h f a) -> GRewriteM m (Cxt h f a) Source #

Applies a rewrite to the first node where it can succeed in a bottom-up traversal. Defined: onebuR f = oneR (onebuR f) <+ f

Ignores holes.

idR :: Applicative m => RewriteM m f l Source #

The identity rewrite

traceR :: forall (f :: (Type -> Type) -> Type -> Type) (a :: Type -> Type) m h l. (ShowHF f, KShow a, HTraversable f, Monad m) => RewriteM m (Cxt h f a) l Source #

Wraps a rewrite with one that performs a debug-print of each visited node

isSortR :: forall l l' f m. (MonadPlus m, DynCase f l) => RewriteM m f l' Source #

isSortR @l performs the identity rewrite at terms of sort l, and fails for all other terms.

Translations

Core types

type Translate (f :: Type -> Type) l t = TranslateM Identity f l t Source #

A single-sorted translation in the Identity monad

type TranslateM (m :: Type -> Type) (f :: Type -> Type) l t = f l -> m t Source #

A monadic translation for a single sort

type GTranslateM (m :: Type -> Type) (f :: Type -> Type) t = forall l. TranslateM m f l t Source #

A monadic translation for all sorts

Conditions

guardBoolT :: MonadPlus m => TranslateM m f l Bool -> TranslateM m f l () Source #

Takes a boolean function of a term, and converts False values to failure in the monad

guardedT :: Alternative m => TranslateM m f l t -> TranslateM m f l u -> TranslateM m f l u -> TranslateM m f l u Source #

Guarded choice: guardedT g t e runs t ("then branch") on its input if g succeeds, and otherwise runs e ("else branch")

Traversals

foldtdT :: forall (f :: (Type -> Type) -> Type -> Type) t (m :: Type -> Type). (HFoldable f, Monoid t, Monad m) => GTranslateM m (HFix f) t -> GTranslateM m (HFix f) t Source #

Fold a tree in a top-down manner. Includes some rudimentary parallelism.

crushtdT :: forall (f :: (Type -> Type) -> Type -> Type) t (m :: Type -> Type). (HFoldable f, Monoid t, Monad m) => GTranslateM (MaybeT m) (HFix f) t -> GTranslateM m (HFix f) t Source #

An always successful top-down fold, replacing failures with mempty.

onetdT :: forall (m :: Type -> Type) (f :: (Type -> Type) -> Type -> Type) t. (MonadPlus m, HFoldable f) => GTranslateM m (HFix f) t -> GTranslateM m (HFix f) t Source #

Runs a translation in a top-down manner, combining its effects. Succeeds if any succeeds. When run using MaybeT, returns its result for the last node where it succeded

pruningCrushtdTF :: forall (f :: (Type -> Type) -> Type -> Type) t (m :: Type -> Type). (HFoldable f, Monoid t, Alternative m) => GTranslateM m (HFix f) t -> GTranslateM m (HFix f) t Source #

Similar to crushtdT, except it never recurses below successes

pruningCrushtdT :: forall (f :: (Type -> Type) -> Type -> Type) t (m :: Type -> Type). (HFoldable f, Monoid t, Monad m) => GTranslateM (MaybeT m) (HFix f) t -> GTranslateM m (HFix f) t Source #

pruningCrushtdTF, replacing top-level failure with mempty

maximalSubterms :: forall (f :: (Type -> Type) -> Type -> Type) l l'. (DynCase (HFix f) l, HFoldable f) => HFix f l' -> [HFix f l] Source #

Gives all subterms of any given sort of a term which are not contained in another term of that sort

(+>>) :: Monad m => TranslateM m f l t -> TranslateM m f l u -> TranslateM m f l u Source #

f + g runs f and g in sequence, ignoring the output of f, and returning the output of g.

isSortT :: forall l l' f m. (DynCase f l, Applicative m) => TranslateM m f l' Bool Source #

isSortT @l is the translate that succeeds for terms of sort l, and fails elsewhere

failT :: Alternative m => TranslateM m f l t Source #

The translation that always fails

notT :: Alternative m => TranslateM m f l t -> RewriteM m f l Source #

Takes a translation, and replaces success with failure, and replaces failure with the identity rewrite

promoteTF :: (DynCase f l, Alternative m) => TranslateM m f l t -> GTranslateM m f t Source #

Allows a one-sorted translation to be applied to any sort, failing at sorts different form the original

mtryM :: (Applicative m, Monoid a) => MaybeT m a -> m a Source #

Runs a failable computation, replacing failure with mempty

foldT :: forall (f :: (Type -> Type) -> Type -> Type) t m l. (HFoldable f, Monoid t, Applicative m) => GTranslateM m (HFix f) t -> TranslateM m (HFix f) l t Source #

Runs a translation on each node which returns a value in some monoid, and combines the results.