Safe Haskell	Safe-Inferred
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 Source # 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 Source # 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.