Language.REST.ExploredTerms

This module implements the optimizations to prune the exploration of rewrites of terms that have been already considered (section 6.4 of the REST paper).

Documentation

data ExploredTerms term c m

A mapping of terms, to the rewritten terms that need to be fully explored | in order for this term to be fully explored

empty :: ExploreFuncs term c m -> ExploreStrategy -> ExploredTerms term c m

insert :: (Eq term, Hashable term) => term -> c -> HashSet term -> ExploredTerms term c m -> ExploredTerms term c m

shouldExplore :: forall term c m. (Monad m, Eq term, Hashable term, Eq c, Show c, Hashable c) => term -> c -> ExploredTerms term c m -> m Bool

shouldExplore t c et determines if rewrites originating from term t at constraints c should be considered, given the already explored terms of et and the associated ExploreStrategy

size :: ExploredTerms term c m -> Int

visited :: (Eq term, Hashable term) => term -> ExploredTerms term c m -> Bool

data ExploreFuncs term c m

Constructors

EF

Fields

• union :: c -> c -> c

  When a term t is visited at constraints c0, and then at constraints c1, the constraints for term t is set to c0 union c1

• subsumes :: c -> c -> m Bool

  c0 subsumes c1 if c0 permits all orderings permited by c1

• exRefine :: c -> term -> term -> c

  exRefine c t u strengthens constraints c to permit the rewrite step from t to u. This is used to determine if considering term u by rewriting from t would permit more rewrite applications.

data ExploreStrategy

ExploreStrategy defines how shouldExplore should decide whether or not | to consider rewrites from a given term

Constructors

ExploreAlways

Always explore, even when it's not necessary.

ExploreLessConstrained

Explore terms unless the constraints are stricter. This may stil explore unnecessary paths, the terms were already fully explored with the different constraints.

ExploreWhenNeeded

Explore terms unless the constraints are stricter OR if all terms reachable via transitive rewrites were already explored.

ExploreOnce

Explore each term only once. This may cause some terms not to be explored if the terms leading to them were initially visited at strict constraints.