Safe Haskell	None

LogicGrowsOnTrees.Checkpoint

Contents

Types
- Cursors and contexts
- Exploration state
Exceptions
Utility functions
Stepper functions
Exploration functions

Description

This module contains the infrastructure used to maintain a checkpoint during a tree exploration.

Synopsis

Types

data Checkpoint Source

Information about the parts of a tree that have been explored.

Constructors

CachePoint ByteString Checkpoint
ChoicePoint Checkpoint Checkpoint
Explored
Unexplored

Instances

Eq Checkpoint
Ord Checkpoint
Read Checkpoint
Show Checkpoint
Monoid Checkpoint	The `Monoid` instance is designed to take checkpoints from two different explorations of a given tree and merge them together to obtain a checkpoint that indicates all of the areas that have been explored by anyone so far. For example, if the two checkpoints are `ChoicePoint Explored Unexplored` and `ChoicePoint Unexplored (ChoicePoint Explored Unexplored)` then the result will be `ChoicePoint Explored (ChoicePoint Explored Unexplored)`. WARNING: This `Monoid` instance is a partial function that expects checkpoints that have come from the same tree; if this precondition is not met then if you are lucky it will notice the inconsistency and throw an exception to let you know that something is wrong and if you are not then it will silently give you a nonsense result. You are very unlikely to run into this problem unless for some reason you are juggling multiple trees and have mixed up which checkpoint goes with which, which is something that is neither done nor encouraged in this package.
Serialize Checkpoint

data Progress α Source

Information about both the current checkpoint and the results we have gathered so far.

Constructors

Progress
Fields progressCheckpoint :: Checkpoint progressResult :: α

Instances

Functor Progress
Eq α => Eq (Progress α)
Show α => Show (Progress α)
Monoid α_1627452025 => Monoid (Progress α_1627452025)
Serialize α_1627452025 => Serialize (Progress α_1627452025)

Cursors and contexts

The types in this subsection are essentially two kinds of zippers for the Checkpoint type; as we explore a tree they represent where we are and how how to backtrack. The difference between the two types that do this is that, at each branch, Context keeps around the subtree for the other branch whereas CheckpointCursor does not. The reason for there being two different types is workload stealing; specifically, when a branch has been stolen from us we want to forget about its subtree because we are no longer going to explore that branch ourselves; thus, workload stealing converts ContextSteps to CheckpointDifferentials. Put another way, as a worker (implemented in LogicGrowsOnTrees.Parallel.Common.Worker) explores the tree at all times it has a CheckpointCursor which tells us about the decisions that it made which are frozen as we will never backtrack into them to explore the other branch and a Context which tells us about where we need to backtrack to explore the rest of the workload assigned to us.

type CheckpointCursor = Seq CheckpointDifferential Source

A zipper that allows us to zoom in on a particular point in the checkpoint.

data CheckpointDifferential Source

The derivative of Checkpoint, used to implement the zipper type CheckpointCursor.

Constructors

CachePointD ByteString
ChoicePointD BranchChoice Checkpoint

Instances

Eq CheckpointDifferential
Read CheckpointDifferential
Show CheckpointDifferential

type Context m α = [ContextStep m α]Source

Like CheckpointCursor, but each step keeps track of the subtree for the alternative branch in case we backtrack to it.

data ContextStep m α Source

Like CheckpointDifferential, but left branches include the subtree for the right branch; the right branches do not need this information because we always explore the left branch first.

Constructors

CacheContextStep ByteString
LeftBranchContextStep Checkpoint (TreeT m α)
RightBranchContextStep

Instances

Show (ContextStep m α)

Exploration state

data ExplorationTState m α Source

The current state of the exploration of a tree starting from a checkpoint.

Constructors

ExplorationTState
Fields explorationStateContext :: !(Context m α) explorationStateCheckpoint :: !Checkpoint explorationStateTree :: !(TreeT m α)

type ExplorationState = ExplorationTState Identity Source

An alias for ExplorationTState in a pure setting.

initialExplorationState :: Checkpoint -> TreeT m α -> ExplorationTState m αSource

Constructs the initial ExplorationTState for the given tree.

Exceptions

data InconsistentCheckpoints Source

This exception is thrown when one attempts to merge checkpoints that disagree with each other; this will never happen as long as you only merge checkpoints that came from the same tree, so if you get this exception then there is almost certainly a bug in your code.

Constructors

InconsistentCheckpoints Checkpoint Checkpoint

Instances

Eq InconsistentCheckpoints
Show InconsistentCheckpoints
Typeable InconsistentCheckpoints
Exception InconsistentCheckpoints

Utility functions

Checkpoint construction

checkpointFromContext :: Context m α -> Checkpoint -> Checkpoint Source

Constructs a full checkpoint given a (context) checkpoint zipper with a hole at your current location and the subcheckpoint at your location.

checkpointFromCursor :: CheckpointCursor -> Checkpoint -> Checkpoint Source

Constructs a full checkpoint given a (cursor) checkpoint zipper with a hole at your current location and the subcheckpoint at your location.

checkpointFromExplorationState :: ExplorationTState m α -> Checkpoint Source

Computes the current checkpoint given the state of an exploration.

checkpointFromReversedList :: (α -> Checkpoint -> Checkpoint) -> [α] -> Checkpoint -> Checkpoint Source

Incrementally builds up a full checkpoint given a sequence corresponding to some cursor at a particular location of the full checkpoint and the subcheckpoint to splice in at that location.

The main reason that you should use this function is that, as it builds up the full checkpoint, it makes some important simplifications via. simplifyCheckpointRoot, such as replacing ChoicePoint Explored Explored with Explored, which both shrinks the size of the checkpoint as well as making it much easier to determine if it is equivalent to Explored.

checkpointFromSequence :: (α -> Checkpoint -> Checkpoint) -> Seq α -> Checkpoint -> Checkpoint Source

The same as checkpointFromReversedList, but where the cursor is specified as a (non-reversed) Seq rather than a list.

checkpointFromInitialPath :: Path -> Checkpoint -> Checkpoint Source

Constructs a full checkpoint given the path to where you are currently searching and the subcheckpoint at your location, assuming that we have no knowledge of anything outside our location (which is indicated by marking it as Unexplored).

checkpointFromUnexploredPath :: Path -> Checkpoint Source

Constructs a full checkpoint given the path to where you are currently located, assuming that the current location is Unexplored and everything outside of our location has been fully explored already.

simplifyCheckpointRoot :: Checkpoint -> Checkpoint Source

Simplifies the root of the checkpoint by replacing

Choicepoint Unexplored Unexplored with Unexplored;
Choicepoint Explored Explored with Explored; and
CachePoint _ Explored with Explored.

simplifyCheckpoint :: Checkpoint -> Checkpoint Source

Applies simplifyCheckpointRoot everywhere in the checkpoint starting from the bottom up.

Path construction

pathFromContext :: Context m α -> Path Source

Computes the path to the current location in the checkpoint as given by the context. (Note that this is a lossy conversation because the resulting path does not contain any information about the branches not taken.)

pathFromCursor :: CheckpointCursor -> Path Source

Computes the path to the current location in the checkpoint as given by the cursor. (Note that this is a lossy conversation because the resulting path does not contain any information about the branches not taken.)

pathStepFromContextStep :: ContextStep m α -> Step Source

Converts a context step to a path step by throwing away information about the alternative branch (if present).

pathStepFromCursorDifferential :: CheckpointDifferential -> Step Source

Converts a cursor differential to a path step by throwing away information about the alternative branch (if present).

Miscelaneous

invertCheckpoint :: Checkpoint -> Checkpoint Source

Inverts a checkpoint so that unexplored areas become explored areas and vice versa. This function satisfies the law that if you sum the result of exploring the tree with the original checkpoint and the result of summing the tree with the inverted checkpoint then (assuming the result monoid commutes) you will get the same result as exploring the entire tree. That is to say,

exploreTreeStartingFromCheckpoint checkpoint tree
<>
exploreTreeStartingFromCheckpoint (invertCheckpoint checkpoint) tree
==
exploreTree tree

Stepper functions

The two functions in the in this section are some of the most important functions in the LogicGrowsOnTrees package, as they provide a means of incrementally exploring a tree starting from a given checkpoint. The functionality provided is sufficiently generic that is used by all the various modes of exploring the tree.

stepThroughTreeStartingFromCheckpoint :: ExplorationState α -> (Maybe α, Maybe (ExplorationState α))Source

Given the current state of exploration, perform an additional step of exploration, returning any solution that was found and the next state of the exploration --- which will be Nothing if the entire tree has been explored.

stepThroughTreeTStartingFromCheckpoint :: Monad m => ExplorationTState m α -> m (Maybe α, Maybe (ExplorationTState m α))Source

Like stepThroughTreeStartingFromCheckpoint, but for an impure tree.

Exploration functions

The functions in this section explore the remainder of a tree, starting from the given checkpoint.

exploreTreeStartingFromCheckpoint :: Monoid α => Checkpoint -> Tree α -> αSource

Explores the remaining nodes in a pure tree, starting from the given checkpoint, and sums over all the results in the leaves.

exploreTreeTStartingFromCheckpoint :: (Monad m, Monoid α) => Checkpoint -> TreeT m α -> m αSource

Explores the remaining nodes in an impure tree, starting from the given checkpoint, and sums over all the results in the leaves.

exploreTreeUntilFirstStartingFromCheckpoint :: Checkpoint -> Tree α -> Maybe αSource

Explores all the remaining nodes in a pure tree, starting from the given checkpoint, until a result (i.e., a leaf) has been found; if a result has been found then it is returned wrapped in Just, otherwise Nothing is returned.

exploreTreeTUntilFirstStartingFromCheckpoint :: Monad m => Checkpoint -> TreeT m α -> m (Maybe α)Source

Same as exploreTreeUntilFirstStartingFromCheckpoint, but for an impure tree.

exploreTreeUntilFoundStartingFromCheckpoint :: Monoid α => (α -> Bool) -> Checkpoint -> Tree α -> (α, Bool)Source

Explores all the remaining nodes in a tree, starting from the given checkpoint and summing all results encountered (i.e., in the leaves) until the current partial sum satisfies the condition provided by the first parameter.

See exploreTreeUntilFound for more details.

exploreTreeTUntilFoundStartingFromCheckpoint :: (Monad m, Monoid α) => (α -> Bool) -> Checkpoint -> TreeT m α -> m (α, Bool)Source

Same as exploreTreeUntilFoundStartingFromCheckpoint, but for an impure tree.