Safe Haskell	Safe-Inferred
Language	Haskell2010

Language.REST.ExploredTerms

Description

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).

Synopsis

data ExploredTerms term c m
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
size :: ExploredTerms term c m -> Int
visited :: (Eq term, Hashable term) => term -> ExploredTerms term c m -> Bool
data ExploreFuncs term c m = EF {
- union :: c -> c -> c
- subsumes :: c -> c -> m Bool
- exRefine :: c -> term -> term -> c
}
data ExploreStrategy

Documentation

data ExploredTerms term c m Source #

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 Source #

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

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 Source #

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 Source #

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

data ExploreFuncs term c m Source #

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 Source #

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.