Ideas.Common.Strategy

A strategy is a context-free grammar with rules as symbols. Strategies can be labeled with strings. The type class IsStrategy is introduced to lift functions and combinators that work on strategies to also accept rules and labeled strategies. This module re-exports the most important functionality of the underlying modules.

Data types and type classes

data Strategy a

Abstract data type for strategies

Instances

Apply Strategy

Methods

applyAll :: Strategy a -> a -> [a]

LiftView Strategy

Methods

liftView :: View a b -> Strategy b -> Strategy a

liftViewIn :: View a (b, c) -> Strategy b -> Strategy a

IsStrategy Strategy

Methods

toStrategy :: Strategy a -> Strategy a

Show (Strategy a)

Methods

showsPrec :: Int -> Strategy a -> ShowS

show :: Strategy a -> String

showList :: [Strategy a] -> ShowS

Fix (Strategy a)

Methods

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

Choice (Strategy a)

Methods

empty :: Strategy a

(.|.) :: Strategy a -> Strategy a -> Strategy a

(./.) :: Strategy a -> Strategy a -> Strategy a

(|>) :: Strategy a -> Strategy a -> Strategy a

choice :: [Strategy a] -> Strategy a

preference :: [Strategy a] -> Strategy a

orelse :: [Strategy a] -> Strategy a

Sequence (Strategy a)

Associated Types

type Sym (Strategy a) :: *

Methods

done :: Strategy a

(~>) :: Sym (Strategy a) -> Strategy a -> Strategy a

(.*.) :: Strategy a -> Strategy a -> Strategy a

single :: Sym (Strategy a) -> Strategy a

sequence :: [Strategy a] -> Strategy a

type Sym (Strategy a)

type Sym (Strategy a) = Rule a

data LabeledStrategy a

A strategy which is labeled with an identifier

Instances

Apply LabeledStrategy

Methods

applyAll :: LabeledStrategy a -> a -> [a]

LiftView LabeledStrategy

Methods

liftView :: View a b -> LabeledStrategy b -> LabeledStrategy a

liftViewIn :: View a (b, c) -> LabeledStrategy b -> LabeledStrategy a

IsStrategy LabeledStrategy

Methods

toStrategy :: LabeledStrategy a -> Strategy a

Show (LabeledStrategy a)

Methods

showsPrec :: Int -> LabeledStrategy a -> ShowS

show :: LabeledStrategy a -> String

showList :: [LabeledStrategy a] -> ShowS

HasId (LabeledStrategy a)

Methods

getId :: LabeledStrategy a -> Id

changeId :: (Id -> Id) -> LabeledStrategy a -> LabeledStrategy a

class IsStrategy f where

Type class to turn values into strategies

Minimal complete definition

toStrategy

Methods

toStrategy :: f a -> Strategy a

Instances

IsStrategy RewriteRule

Methods

toStrategy :: RewriteRule a -> Strategy a

IsStrategy Rule

Methods

toStrategy :: Rule a -> Strategy a

IsStrategy Dynamic

Methods

toStrategy :: Dynamic a -> Strategy a

IsStrategy LabeledStrategy

Methods

toStrategy :: LabeledStrategy a -> Strategy a

IsStrategy Strategy

Methods

toStrategy :: Strategy a -> Strategy a

Running strategies

derivationList :: IsStrategy f => (Rule a -> Rule a -> Ordering) -> f a -> a -> [Derivation (Rule a, Environment) a]

Strategy combinators

Basic combinators

(.*.) :: (IsStrategy f, IsStrategy g) => f a -> g a -> Strategy a infixr 5

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

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

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

(.%.) :: (IsStrategy f, IsStrategy g) => f a -> g a -> Strategy a infixr 2

Interleave two strategies

(.@.) :: (IsStrategy f, IsStrategy g) => f a -> g a -> Strategy a infixr 2

Alternate two strategies

(!~>) :: IsStrategy f => Rule a -> f a -> Strategy a infixr 5

Prefixing a basic rule to a strategy atomically

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 an identifier. Labels are used to identify substrategies and to specialize feedback messages. The first argument of label can be of type String, in which case the string is used as identifier (and not as description).

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

Initial prefixes (allows the strategy to stop succesfully at any time)

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

Puts a list of strategies into a sequence

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

Combines a list of alternative strategies

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

Combines a list of strategies with left-preference

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

Combines a list of strategies with left-biased choice

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

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

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 infixr 4

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

(./.) :: (IsStrategy f, IsStrategy g) => f a -> g a -> Strategy a infixr 4

Choose between the two strategies, with a preference for steps from the left hand-side 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

dynamic :: (IsId n, IsStrategy f, IsTerm a) => n -> (a -> f a) -> Strategy a

The structure of a dynamic strategy depends on the current term

Graph

type DependencyGraph node key = [(node, key, [key])]

dependencyGraph :: (IsStrategy f, Ord key) => DependencyGraph (f a) key -> Strategy a

Create a strategy from a dependency graph with strategies as nodes Does not check for cycles

Traversal combinators

module Ideas.Common.Strategy.Traversal

Configuration combinators

module Ideas.Common.Strategy.Configuration

Strategy locations

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

Returns a list of all strategy locations, paired with the label

checkLocation :: Id -> LabeledStrategy a -> Bool

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

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

Prefixes

data Prefix a

Instances

Show (Prefix a)

Methods

showsPrec :: Int -> Prefix a -> ShowS

show :: Prefix a -> String

showList :: [Prefix a] -> ShowS

Semigroup (Prefix a)

Methods

(<>) :: Prefix a -> Prefix a -> Prefix a

sconcat :: NonEmpty (Prefix a) -> Prefix a

stimes :: Integral b => b -> Prefix a -> Prefix a

Monoid (Prefix a)

Methods

mempty :: Prefix a

mappend :: Prefix a -> Prefix a -> Prefix a

mconcat :: [Prefix a] -> Prefix a

Firsts (Prefix a)

Associated Types

type Elem (Prefix a) :: *

Methods

ready :: Prefix a -> Bool

firsts :: Prefix a -> [(Elem (Prefix a), Prefix a)]

type Elem (Prefix a)

type Elem (Prefix a) = (Rule a, a, Environment)

emptyPrefix :: IsStrategy f => f a -> a -> Prefix a

Construct the empty prefix for a labeled strategy

noPrefix :: Prefix a

The error prefix (i.e., without a location in the strategy).

replayPath :: IsStrategy f => Path -> f a -> a -> ([Rule a], Prefix a)

Construct a prefix for a path and a labeled strategy. The third argument is the current term.

replayPaths :: IsStrategy f => [Path] -> f a -> a -> Prefix a

Construct a prefix for a list of paths and a labeled strategy. The third argument is the current term.

replayStrategy :: (Monad m, IsStrategy f) => Path -> f a -> a -> m (a, Prefix a)

Construct a prefix for a path and a labeled strategy. The third argument is the initial term.

data Path

A path encodes a location in a strategy. Paths are represented as a list of integers and terms (the latter act as input for the dynamic strategies).

Instances

Eq Path

Methods

(==) :: Path -> Path -> Bool

(/=) :: Path -> Path -> Bool

Show Path

Methods

showsPrec :: Int -> Path -> ShowS

show :: Path -> String

showList :: [Path] -> ShowS

emptyPath :: Path

The empty path.

readPath :: Monad m => String -> m Path

readPaths :: Monad m => String -> m [Path]

prefixPaths :: Prefix a -> [Path]

Returns the current Path.

majorPrefix :: Prefix a -> Prefix a

Transforms the prefix such that only major steps are kept in the remaining strategy.

isEmptyPrefix :: Prefix a -> Bool

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