LogicGrowsOnTrees.Checkpoint

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

Types

data Checkpoint

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 α

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 α_1627452313 => Monoid (Progress α_1627452313)

Serialize α_1627452313 => Serialize (Progress α_1627452313)

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

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

data CheckpointDifferential

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 α]

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

data ContextStep m α

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 α

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

An alias for ExplorationTState in a pure setting.

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

Constructs the initial ExplorationTState for the given tree.

Exceptions

data InconsistentCheckpoints

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

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

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

Computes the current checkpoint given the state of an exploration.

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

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

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

checkpointFromInitialPath :: Path -> Checkpoint -> Checkpoint

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

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

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

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

Path construction

pathFromContext :: Context m α -> Path

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

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

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

pathStepFromCursorDifferential :: CheckpointDifferential -> Step

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

Miscelaneous

invertCheckpoint :: Checkpoint -> Checkpoint

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

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

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 α -> α

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 α

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 α

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

Same as exploreTreeUntilFirstStartingFromCheckpoint, but for an impure tree.

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

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)

Same as exploreTreeUntilFoundStartingFromCheckpoint, but for an impure tree.