Safe Haskell	None
Language	Haskell2010

Data.Equality.Saturation.Scheduler

Description

Definition of Scheduler as a way to control application of rewrite rules.

The BackoffScheduler is a scheduler which implements exponential rule backoff and is used by default in equalitySaturation

Synopsis

class Scheduler s where
- data Stat s
- updateStats :: s -> Int -> Int -> Maybe (Stat s) -> IntMap (Stat s) -> [Match] -> IntMap (Stat s)
- isBanned :: Int -> Stat s -> Bool
data BackoffScheduler = BackoffScheduler {
- matchLimit :: !Int
- banLength :: !Int
}
defaultBackoffScheduler :: BackoffScheduler

Documentation

class Scheduler s where Source #

A Scheduler determines whether a certain rewrite rule is banned from being used based on statistics it defines and collects on applied rewrite rules.

Associated Types

data Stat s Source #

Methods

updateStats Source #

Arguments

:: s	The scheduler itself
-> Int	Iteration we're in
-> Int	Index of rewrite rule we're updating
-> Maybe (Stat s)	Current stat for this rewrite rule (we already got it so no point in doing a lookup again)
-> IntMap (Stat s)	The current stats map
-> [Match]	The list of matches resulting from matching this rewrite rule
-> IntMap (Stat s)	The updated map with new stats

Scheduler: update stats

isBanned Source #

Arguments

:: Int	Iteration we're in
-> Stat s	Stats for the rewrite rule
-> Bool	Whether the rule should be applied or not

Instances

Instances details

Scheduler BackoffScheduler Source #

Instance details

Defined in Data.Equality.Saturation.Scheduler

Associated Types

data Stat BackoffScheduler
Instance details Defined in Data.Equality.Saturation.Scheduler data Stat BackoffScheduler = BSS { bannedUntil :: !Int timesBanned :: !Int }

Methods

updateStats :: BackoffScheduler -> Int -> Int -> Maybe (Stat BackoffScheduler) -> IntMap (Stat BackoffScheduler) -> [Match] -> IntMap (Stat BackoffScheduler) Source #

isBanned :: Int -> Stat BackoffScheduler -> Bool Source #

data BackoffScheduler Source #

A Scheduler that implements exponentional rule backoff.

For each rewrite, there exists a configurable initial match limit. If a rewrite search yield more than this limit, then we ban this rule for number of iterations, double its limit, and double the time it will be banned next time.

This seems effective at preventing explosive rules like associativity from taking an unfair amount of resources.

Originaly in egg

Constructors

BackoffScheduler
Fields matchLimit :: !Int banLength :: !Int

Instances

Instances details

Scheduler BackoffScheduler Source #

Instance details

Defined in Data.Equality.Saturation.Scheduler

Associated Types

data Stat BackoffScheduler
Instance details Defined in Data.Equality.Saturation.Scheduler data Stat BackoffScheduler = BSS { bannedUntil :: !Int timesBanned :: !Int }

Methods

updateStats :: BackoffScheduler -> Int -> Int -> Maybe (Stat BackoffScheduler) -> IntMap (Stat BackoffScheduler) -> [Match] -> IntMap (Stat BackoffScheduler) Source #

isBanned :: Int -> Stat BackoffScheduler -> Bool Source #

Show (Stat BackoffScheduler) Source #

Instance details

Defined in Data.Equality.Saturation.Scheduler

Methods

showsPrec :: Int -> Stat BackoffScheduler -> ShowS #

show :: Stat BackoffScheduler -> String #

showList :: [Stat BackoffScheduler] -> ShowS #

data Stat BackoffScheduler Source #

Instance details

Defined in Data.Equality.Saturation.Scheduler

data Stat BackoffScheduler = BSS {

bannedUntil :: !Int
timesBanned :: !Int

}

defaultBackoffScheduler :: BackoffScheduler Source #

The default BackoffScheduler.

The match limit is set to 1000 and the ban length is set to 10.