Copyright	(c) Galois Inc 2025
License	BSD3
Safe Haskell	Safe-Inferred
Language	Haskell2010

Lang.Crucible.Backend.Goals

Contents

Traversals

Description

This module defines a data strucutre for storing a collection of proof obligations, and the current state of assumptions.

Synopsis

data ProofGoal asmp goal = ProofGoal {
- proofAssumptions :: asmp
- proofGoal :: goal
}
data Goals asmp goal
- = Assuming asmp !(Goals asmp goal)
- | Prove goal
- | ProveConj !(Goals asmp goal) !(Goals asmp goal)
ppGoals :: (asmp -> Doc ann) -> (goal -> Doc ann) -> Goals asmp goal -> Doc ann
goalsToList :: Monoid asmp => Goals asmp goal -> [ProofGoal asmp goal]
assuming :: Monoid asmp => asmp -> Goals asmp goal -> Goals asmp goal
proveAll :: Foldable t => t (Goals asmp goal) -> Maybe (Goals asmp goal)
goalsConj :: Maybe (Goals asmp goal) -> Maybe (Goals asmp goal) -> Maybe (Goals asmp goal)
traverseGoals :: (Applicative f, Monoid asmp') => (forall a. asmp -> f a -> f (asmp', a)) -> (goal -> f (Maybe goal')) -> Goals asmp goal -> f (Maybe (Goals asmp' goal'))
traverseOnlyGoals :: (Applicative f, Monoid asmp) => (goal -> f (Maybe goal')) -> Goals asmp goal -> f (Maybe (Goals asmp goal'))
traverseGoalsWithAssumptions :: (Applicative f, Monoid asmp) => (asmp -> goal -> f (Maybe goal')) -> Goals asmp goal -> f (Maybe (Goals asmp goal'))
traverseGoalsSeq :: (Applicative f, Monoid asmp') => (forall a. asmp -> f a -> f (asmp', a)) -> (goal -> f (Maybe goal')) -> Seq (Goals asmp goal) -> f (Seq (Goals asmp' goal'))

Documentation

data ProofGoal asmp goal Source #

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

Constructors

ProofGoal
Fields proofAssumptions :: asmp proofGoal :: goal

data Goals asmp goal Source #

A collection of goals, which can represent shared assumptions.

Constructors

Assuming asmp !(Goals asmp goal)	Make an assumption that is in context for all the contained goals.
Prove goal	A proof obligation, to be proved in the context of all previously-made assumptions.
ProveConj !(Goals asmp goal) !(Goals asmp goal)	A conjunction of two goals.

Instances

Instances details

(Show asmp, Show goal) => Show (Goals asmp goal) Source #
Instance details Defined in Lang.Crucible.Backend.Goals Methods showsPrec :: Int -> Goals asmp goal -> ShowS # show :: Goals asmp goal -> String # showList :: [Goals asmp goal] -> ShowS #
(Pretty asmp, Pretty goal) => Pretty (Goals asmp goal) Source #	Intended for debugging, this is not generally a user-facing datatype.
Instance details Defined in Lang.Crucible.Backend.Goals Methods pretty :: Goals asmp goal -> Doc ann # prettyList :: [Goals asmp goal] -> Doc ann #

ppGoals :: (asmp -> Doc ann) -> (goal -> Doc ann) -> Goals asmp goal -> Doc ann Source #

Intended for debugging, this is not generally a user-facing datatype.

goalsToList :: Monoid asmp => Goals asmp goal -> [ProofGoal asmp goal] Source #

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

assuming :: Monoid asmp => asmp -> Goals asmp goal -> Goals asmp goal Source #

Construct a goal that first assumes a collection of assumptions and then states a goal.

proveAll :: Foldable t => t (Goals asmp goal) -> Maybe (Goals asmp goal) Source #

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.

goalsConj :: Maybe (Goals asmp goal) -> Maybe (Goals asmp goal) -> Maybe (Goals asmp goal) Source #

Helper to conjoin two possibly trivial Goals objects.

Traversals

traverseGoals :: (Applicative f, Monoid asmp') => (forall a. asmp -> f a -> f (asmp', a)) -> (goal -> f (Maybe goal')) -> Goals asmp goal -> f (Maybe (Goals asmp' goal')) Source #

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.

traverseOnlyGoals :: (Applicative f, Monoid asmp) => (goal -> f (Maybe goal')) -> Goals asmp goal -> f (Maybe (Goals asmp goal')) Source #

traverseGoalsWithAssumptions :: (Applicative f, Monoid asmp) => (asmp -> goal -> f (Maybe goal')) -> Goals asmp goal -> f (Maybe (Goals asmp goal')) Source #

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

traverseGoalsSeq :: (Applicative f, Monoid asmp') => (forall a. asmp -> f a -> f (asmp', a)) -> (goal -> f (Maybe goal')) -> Seq (Goals asmp goal) -> f (Seq (Goals asmp' goal')) Source #

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.