Ideas.Common.Strategy

A strategy is a context-free grammar with rules as symbols. Strategies can be labeled with strings. A type class is introduced to lift all the combinators that work on strategies, only to prevent that you have to insert these lifting functions yourself.

Data types and type classes

data Strategy a

Abstract data type for strategies

Instances

Apply Strategy

LiftView Strategy

IsStrategy Strategy

Typed a (Strategy (Context a))

Show (Strategy a)

(Arbitrary a, CoArbitrary a) => Arbitrary (Strategy a)

data LabeledStrategy a

A strategy which is labeled with a string

Instances

Apply LabeledStrategy

LiftView LabeledStrategy

IsLabeled LabeledStrategy

IsStrategy LabeledStrategy

Show (LabeledStrategy a)

HasId (LabeledStrategy a)

class IsStrategy f where

Type class to turn values into strategies

Methods

toStrategy :: f a -> Strategy a

Instances

IsStrategy RewriteRule

IsStrategy Rule

IsStrategy LabeledStrategy

IsStrategy Strategy

Running strategies

fullDerivationTree :: IsStrategy f => Bool -> f a -> a -> DerivationTree (Step LabelInfo a) a

Returns the derivation tree for a strategy and a term, including all minor rules

derivationTree :: IsStrategy f => Bool -> f a -> a -> DerivationTree (Rule a, Environment) a

Returns the derivation tree for a strategy and a term with only major rules

Strategy combinators

Basic combinators

(<*>) :: (IsStrategy f, IsStrategy g) => f a -> g a -> Strategy a

Put two strategies in sequence (first do this, then do that)

(<|>) :: (IsStrategy f, IsStrategy g) => f a -> g a -> Strategy a

Choose between the two strategies (either do this or do that)

(<%>) :: (IsStrategy f, IsStrategy g) => f a -> g a -> Strategy a

Interleave two strategies

succeed :: Strategy a

The strategy that always succeeds (without doing anything)

fail :: Strategy a

The strategy that always fails

atomic :: IsStrategy f => f a -> Strategy a

Makes a strategy atomic (w.r.t. parallel composition)

label :: (IsId l, IsStrategy f) => l -> f a -> LabeledStrategy a

Labels a strategy with a string

sequence :: IsStrategy f => [f a] -> Strategy a

Puts a list of strategies into a sequence

alternatives :: IsStrategy f => [f a] -> Strategy a

Combines a list of alternative strategies

interleave :: IsStrategy f => [f a] -> Strategy a

Merges a list of strategies (in parallel)

permute :: IsStrategy f => [f a] -> Strategy a

Allows all permutations of the list

fix :: (Strategy a -> Strategy a) -> Strategy a

A fix-point combinator on strategies (to model recursion). Powerful (but dangerous) combinator

EBNF combinators

many :: IsStrategy f => f a -> Strategy a

Repeat a strategy zero or more times (non-greedy)

many1 :: IsStrategy f => f a -> Strategy a

Apply a certain strategy at least once (non-greedy)

replicate :: IsStrategy f => Int -> f a -> Strategy a

Apply a strategy a certain number of times

option :: IsStrategy f => f a -> Strategy a

Apply a certain strategy or do nothing (non-greedy)

Negation and greedy combinators

check :: (a -> Bool) -> Strategy a

Checks whether a predicate holds for the current term. The check is considered to be a minor step.

not :: IsStrategy f => f a -> Strategy a

Check whether or not the argument strategy cannot be applied: the result strategy only succeeds if this is not the case (otherwise it fails).

repeat :: IsStrategy f => f a -> Strategy a

Repeat a strategy zero or more times (greedy version of many)

repeat1 :: IsStrategy f => f a -> Strategy a

Apply a certain strategy at least once (greedy version of many1)

try :: IsStrategy f => f a -> Strategy a

Apply a certain strategy if this is possible (greedy version of option)

(|>) :: (IsStrategy f, IsStrategy g) => f a -> g a -> Strategy a

Left-biased choice: if the left-operand strategy can be applied, do so. Otherwise, try the right-operand strategy

exhaustive :: IsStrategy f => [f a] -> Strategy a

Apply the strategies from the list exhaustively (until this is no longer possible)

while :: IsStrategy f => (a -> Bool) -> f a -> Strategy a

Repeat the strategy as long as the predicate holds

until :: IsStrategy f => (a -> Bool) -> f a -> Strategy a

Repeat the strategy until the predicate holds

multi :: (IsId l, IsStrategy f) => l -> f a -> LabeledStrategy a

Apply a strategy at least once, but collapse into a single step

Traversal combinators

module Ideas.Common.Strategy.Traversal

Configuration combinators

module Ideas.Common.Strategy.Configuration

Strategy locations

strategyLocations :: LabeledStrategy a -> [([Int], LabeledStrategy a)]

Returns a list of all strategy locations, paired with the labeled substrategy at that location

subStrategy :: Id -> LabeledStrategy a -> Maybe (LabeledStrategy a)

Returns the substrategy or rule at a strategy location. Nothing indicates that the location is invalid

subTaskLocation :: LabeledStrategy a -> Id -> Id -> Id

nextTaskLocation :: LabeledStrategy a -> Id -> Id -> Id

Prefixes

data Prefix a

Abstract data type for a (labeled) strategy with a prefix (a sequence of executed rules). A prefix is still aware of the labels that appear in the strategy. A prefix is encoded as a list of integers (and can be reconstructed from such a list: see makePrefix). The list is stored in reversed order.

Instances

Eq (Prefix a)

Show (Prefix a)

emptyPrefix :: LabeledStrategy a -> Prefix a

Construct the empty prefix for a labeled strategy

makePrefix :: Monad m => [Int] -> LabeledStrategy a -> m (Prefix a)

Construct a prefix for a given list of integers and a labeled strategy.

prefixTree :: Bool -> Prefix a -> a -> DerivationTree (Prefix a) a

Create a derivation tree with a prefix as annotation.

data Step l a

Constructors

Enter l

Exit l

RuleStep Environment (Rule a)

Instances

Apply (Step l)

Eq l => Eq (Step l a)

Show l => Show (Step l a)

Minor (Step l a)

prefixToSteps :: Prefix a -> [Step LabelInfo a]

stepsToRules :: [Step l a] -> [Rule a]

Retrieves the rules from a list of steps

lastStepInPrefix :: Prefix a -> Maybe (Step LabelInfo a)

Returns the last rule of a prefix (if such a rule exists)

Misc

cleanUpStrategy :: (a -> a) -> LabeledStrategy a -> LabeledStrategy a

Use a function as do-after hook for all rules in a labeled strategy, but also use the function beforehand

cleanUpStrategyAfter :: (a -> a) -> LabeledStrategy a -> LabeledStrategy a

Use a function as do-after hook for all rules in a labeled strategy

rulesInStrategy :: IsStrategy f => f a -> [Rule a]

Returns a list of all major rules that are part of a labeled strategy