A proof goal consists of a collection of assumptions that were in scope when an assertion was made, together with the given assertion.

A collection of goals, which can represent shared assumptions.

Render the tree of goals as a list instead, duplicating shared assumptions over each goal as necessary.

Construct a Goals object from a collection of subgoals, all of which are to be proved. This yields Nothing if the collection of goals is empty, and otherwise builds a conjunction of all the goals. Note that there is no new sharing in the resulting structure.

Helper to conjoin two possibly trivial Goals objects.

Traverse the structure of a Goals data structure. The function for visiting goals my decide to remove the goal from the structure. If no goals remain after the traversal, the resulting value will be a Nothing.

In a call to 'traverseGoals assumeAction transformer goals', the arguments are used as follows:

• traverseGoals is an action is called every time we encounter an Assuming constructor. The first argument is the original sequence of assumptions. The second argument is a continuation action. The result is a sequence of transformed assumptions and the result of the continuation action.
• assumeAction is a transformer action on goals. Return Nothing if you wish to remove the goal from the overall tree.

Visit every goal in a Goals structure, remembering the sequence of assumptions along the way to that goal.

Traverse a sequence of Goals data structures. See traverseGoals for an explanation of the action arguments. The resulting sequence may be shorter than the original if some Goals become trivial.

A FrameIdentifier is a value that identifies an an assumption frame. These are expected to be unique when a new frame is pushed onto the stack. This is primarily a debugging aid, to ensure that stack management remains well-bracketed.

A data-structure that can incrementally collect goals in context. It keeps track both of the collection of assumptions that lead to the current state, as well as any proof obligations incurred along the way.

The main use of GoalCollector is as the state of an AssumptionStack, which itself is part of the state of the simple and online backends.

GoalCollector can be somewhat counter-intuitive. The "top" (TopCollector) is the *leaf* when GoalCollector is considered as a tree (which is a common way to conceptualize recursive algebraic data types such as this one). A GoalCollector is shaped like a cons-list with three different cons-like constructors (CollectorFrame, CollectingAssumptions, and CollectingGoals) and one nil-like constructor TopCollector. That is to say, a GoalCollector is a sequence that always ends in a single TopCollector.

Furthermore, the frame identified by the first (FrameIdentifier) argument of CollectorFrame does not conceptually contain the goals *inside* the second (GoalCollector) argument, but rather contains all the assumptions and goals in whatever GoalCollector *contains* the CollectorFrame constructor (everything *outside* of the CollectorFrame). Concretely, in the expression CollectingGoals gls (CollectingAssumptions asmps (CollectorFrame frm (TopCollector gls0))) the goals gls and assumptions asmps are in the frame frm, rather than the top-level goals gls0.

This inside-out structure is reflected in the pretty-printer ppGoalCollector below. The Crucible-CLI test-case assumption-state shows this pretty-printer in action in a Crucible program with branching, which can be helpful in understanding GoalCollector.

A collector with no goals and no context.

Traverse the goals in a 'GoalCollector. See traverseGoals for an explaination of the action arguments.

Traverse the goals in a GoalCollector, keeping track, for each goal, of the assumptions leading to that goal.

Add a sequence of extra assumptions to the current context.

Add a new proof obligation to the current context.

Mark the current frame. Using gcPop will unwind to here.

Pop to the last push, or all the way to the top, if there were no more pushes. If the result is Left, then we popped until an explicitly marked push; in that case we return:

1. the frame identifier of the popped frame,
2. the assumptions that were forgotten,
3. any proof goals that were generated since the frame push, and
4. the state of the collector before the push.

If the result is Right, then we popped all the way to the top, and the result is the goal tree, or Nothing if there were no goals.

Add an assumption that is in scope for all goals, even ones in earlier frames.

Remove all collected proof obligations, but keep the current set of assumptions.

This operation restores the assumption state of the first given GoalCollector, overwriting the assumptions state of the second collector. However, all proof obligations in the second collector are retained and placed into the the first goal collector in the base assumption level.

The end result is a goal collector that maintains all the active proof obligations of both collectors, and has the same assumption context as the first collector.

Reset the goal collector to the empty assumption state; but first collect all the pending proof goals and stash them.

Get all currently collected goals.

The AssumptionFrames data structure captures the current state of assumptions made inside a GoalCollector.

Return a list of all the assumption frames in this goal collector. The first element of the pair is a collection of assumptions made unconditionaly at top level. The remaining list is a sequence of assumption frames, each consisting of a collection of assumptions made in that frame. Frames closer to the front of the list are older. A gcPop will remove the newest (rightmost) frame from the list.