{-|
Module      : Lang.Crucible.Backend.Goals
Copyright   : (c) Galois, Inc 2025
License     : BSD3

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

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TupleSections #-}

module Lang.Crucible.Backend.Goals
  ( ProofGoal(..)
  , Goals(..)
  , goalsToList
  , assuming
  , proveAll
  , goalsConj
    -- * Traversals
  , traverseGoals
  , traverseOnlyGoals
  , traverseGoalsWithAssumptions
  , traverseGoalsSeq
  )
  where

import           Control.Monad.Reader (ReaderT(..), withReaderT)
import           Data.Functor.Const (Const(..))
import           Data.Sequence (Seq)
import qualified Data.Sequence as Seq

-- | A proof goal consists of a collection of assumptions
--   that were in scope when an assertion was made, together
--   with the given assertion.
data ProofGoal asmp goal =
  ProofGoal
  { forall asmp goal. ProofGoal asmp goal -> asmp
proofAssumptions :: asmp
  , forall asmp goal. ProofGoal asmp goal -> goal
proofGoal        :: goal
  }

-- | A collection of goals, which can represent shared assumptions.
data Goals asmp goal =
    -- | Make an assumption that is in context for all the
    --   contained goals.
    Assuming asmp !(Goals asmp goal)

    -- | A proof obligation, to be proved in the context of
    --   all previously-made assumptions.
  | Prove goal

    -- | A conjunction of two goals.
  | ProveConj !(Goals asmp goal) !(Goals asmp goal)
    deriving Int -> Goals asmp goal -> ShowS
[Goals asmp goal] -> ShowS
Goals asmp goal -> String
(Int -> Goals asmp goal -> ShowS)
-> (Goals asmp goal -> String)
-> ([Goals asmp goal] -> ShowS)
-> Show (Goals asmp goal)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall asmp goal.
(Show asmp, Show goal) =>
Int -> Goals asmp goal -> ShowS
forall asmp goal.
(Show asmp, Show goal) =>
[Goals asmp goal] -> ShowS
forall asmp goal.
(Show asmp, Show goal) =>
Goals asmp goal -> String
$cshowsPrec :: forall asmp goal.
(Show asmp, Show goal) =>
Int -> Goals asmp goal -> ShowS
showsPrec :: Int -> Goals asmp goal -> ShowS
$cshow :: forall asmp goal.
(Show asmp, Show goal) =>
Goals asmp goal -> String
show :: Goals asmp goal -> String
$cshowList :: forall asmp goal.
(Show asmp, Show goal) =>
[Goals asmp goal] -> ShowS
showList :: [Goals asmp goal] -> ShowS
Show

-- | Construct a goal that first assumes a collection of
--   assumptions and then states a goal.
assuming :: Monoid asmp => asmp -> Goals asmp goal -> Goals asmp goal
assuming :: forall asmp goal.
Monoid asmp =>
asmp -> Goals asmp goal -> Goals asmp goal
assuming asmp
as (Assuming asmp
bs Goals asmp goal
g) = asmp -> Goals asmp goal -> Goals asmp goal
forall asmp goal.
Monoid asmp =>
asmp -> Goals asmp goal -> Goals asmp goal
assuming (asmp
as asmp -> asmp -> asmp
forall a. Semigroup a => a -> a -> a
<> asmp
bs) Goals asmp goal
g
assuming asmp
as Goals asmp goal
g = asmp -> Goals asmp goal -> Goals asmp goal
forall asmp goal. asmp -> Goals asmp goal -> Goals asmp goal
Assuming asmp
as Goals asmp goal
g

-- | 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.
proveAll :: Foldable t => t (Goals asmp goal) -> Maybe (Goals asmp goal)
proveAll :: forall (t :: Type -> Type) asmp goal.
Foldable t =>
t (Goals asmp goal) -> Maybe (Goals asmp goal)
proveAll = (Goals asmp goal
 -> Maybe (Goals asmp goal) -> Maybe (Goals asmp goal))
-> Maybe (Goals asmp goal)
-> t (Goals asmp goal)
-> Maybe (Goals asmp goal)
forall a b. (a -> b -> b) -> b -> t a -> b
forall (t :: Type -> Type) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Goals asmp goal
-> Maybe (Goals asmp goal) -> Maybe (Goals asmp goal)
forall {asmp} {goal}.
Goals asmp goal
-> Maybe (Goals asmp goal) -> Maybe (Goals asmp goal)
f Maybe (Goals asmp goal)
forall a. Maybe a
Nothing
 where
 f :: Goals asmp goal
-> Maybe (Goals asmp goal) -> Maybe (Goals asmp goal)
f Goals asmp goal
x Maybe (Goals asmp goal)
Nothing  = Goals asmp goal -> Maybe (Goals asmp goal)
forall a. a -> Maybe a
Just (Goals asmp goal -> Maybe (Goals asmp goal))
-> Goals asmp goal -> Maybe (Goals asmp goal)
forall a b. (a -> b) -> a -> b
$! Goals asmp goal
x
 f Goals asmp goal
x (Just Goals asmp goal
y) = Goals asmp goal -> Maybe (Goals asmp goal)
forall a. a -> Maybe a
Just (Goals asmp goal -> Maybe (Goals asmp goal))
-> Goals asmp goal -> Maybe (Goals asmp goal)
forall a b. (a -> b) -> a -> b
$! Goals asmp goal -> Goals asmp goal -> Goals asmp goal
forall asmp goal.
Goals asmp goal -> Goals asmp goal -> Goals asmp goal
ProveConj Goals asmp goal
x Goals asmp goal
y

-- | Helper to conjoin two possibly trivial 'Goals' objects.
goalsConj :: Maybe (Goals asmp goal) -> Maybe (Goals asmp goal) -> Maybe (Goals asmp goal)
goalsConj :: forall asmp goal.
Maybe (Goals asmp goal)
-> Maybe (Goals asmp goal) -> Maybe (Goals asmp goal)
goalsConj Maybe (Goals asmp goal)
Nothing Maybe (Goals asmp goal)
y = Maybe (Goals asmp goal)
y
goalsConj Maybe (Goals asmp goal)
x Maybe (Goals asmp goal)
Nothing = Maybe (Goals asmp goal)
x
goalsConj (Just Goals asmp goal
x) (Just Goals asmp goal
y) = Goals asmp goal -> Maybe (Goals asmp goal)
forall a. a -> Maybe a
Just (Goals asmp goal -> Goals asmp goal -> Goals asmp goal
forall asmp goal.
Goals asmp goal -> Goals asmp goal -> Goals asmp goal
ProveConj Goals asmp goal
x Goals asmp goal
y)

-- | Render the tree of goals as a list instead, duplicating
--   shared assumptions over each goal as necessary.
goalsToList :: Monoid asmp => Goals asmp goal -> [ProofGoal asmp goal]
goalsToList :: forall asmp goal.
Monoid asmp =>
Goals asmp goal -> [ProofGoal asmp goal]
goalsToList =
  Const [ProofGoal asmp goal] (Maybe (Goals asmp Any))
-> [ProofGoal asmp goal]
forall {k} a (b :: k). Const a b -> a
getConst (Const [ProofGoal asmp goal] (Maybe (Goals asmp Any))
 -> [ProofGoal asmp goal])
-> (Goals asmp goal
    -> Const [ProofGoal asmp goal] (Maybe (Goals asmp Any)))
-> Goals asmp goal
-> [ProofGoal asmp goal]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (asmp -> goal -> Const [ProofGoal asmp goal] (Maybe Any))
-> Goals asmp goal
-> Const [ProofGoal asmp goal] (Maybe (Goals asmp Any))
forall (f :: Type -> Type) asmp goal goal'.
(Applicative f, Monoid asmp) =>
(asmp -> goal -> f (Maybe goal'))
-> Goals asmp goal -> f (Maybe (Goals asmp goal'))
traverseGoalsWithAssumptions
    (\asmp
as goal
g -> [ProofGoal asmp goal] -> Const [ProofGoal asmp goal] (Maybe Any)
forall {k} a (b :: k). a -> Const a b
Const [asmp -> goal -> ProofGoal asmp goal
forall asmp goal. asmp -> goal -> ProofGoal asmp goal
ProofGoal asmp
as goal
g])

-- | 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.
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'))
traverseGoals :: forall (f :: Type -> Type) asmp' asmp goal goal'.
(Applicative f, Monoid asmp') =>
(forall a. asmp -> f a -> f (asmp', a))
-> (goal -> f (Maybe goal'))
-> Goals asmp goal
-> f (Maybe (Goals asmp' goal'))
traverseGoals forall a. asmp -> f a -> f (asmp', a)
fas goal -> f (Maybe goal')
fgl = Goals asmp goal -> f (Maybe (Goals asmp' goal'))
go
  where
  go :: Goals asmp goal -> f (Maybe (Goals asmp' goal'))
go (Prove goal
gl)        = (goal' -> Goals asmp' goal')
-> Maybe goal' -> Maybe (Goals asmp' goal')
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap goal' -> Goals asmp' goal'
forall asmp goal. goal -> Goals asmp goal
Prove (Maybe goal' -> Maybe (Goals asmp' goal'))
-> f (Maybe goal') -> f (Maybe (Goals asmp' goal'))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> goal -> f (Maybe goal')
fgl goal
gl
  go (Assuming asmp
as Goals asmp goal
gl)  = (asmp', Maybe (Goals asmp' goal')) -> Maybe (Goals asmp' goal')
forall {asmp} {goal}.
Monoid asmp =>
(asmp, Maybe (Goals asmp goal)) -> Maybe (Goals asmp goal)
assuming' ((asmp', Maybe (Goals asmp' goal')) -> Maybe (Goals asmp' goal'))
-> f (asmp', Maybe (Goals asmp' goal'))
-> f (Maybe (Goals asmp' goal'))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> asmp
-> f (Maybe (Goals asmp' goal'))
-> f (asmp', Maybe (Goals asmp' goal'))
forall a. asmp -> f a -> f (asmp', a)
fas asmp
as (Goals asmp goal -> f (Maybe (Goals asmp' goal'))
go Goals asmp goal
gl)
  go (ProveConj Goals asmp goal
g1 Goals asmp goal
g2) = Maybe (Goals asmp' goal')
-> Maybe (Goals asmp' goal') -> Maybe (Goals asmp' goal')
forall asmp goal.
Maybe (Goals asmp goal)
-> Maybe (Goals asmp goal) -> Maybe (Goals asmp goal)
goalsConj (Maybe (Goals asmp' goal')
 -> Maybe (Goals asmp' goal') -> Maybe (Goals asmp' goal'))
-> f (Maybe (Goals asmp' goal'))
-> f (Maybe (Goals asmp' goal') -> Maybe (Goals asmp' goal'))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Goals asmp goal -> f (Maybe (Goals asmp' goal'))
go Goals asmp goal
g1 f (Maybe (Goals asmp' goal') -> Maybe (Goals asmp' goal'))
-> f (Maybe (Goals asmp' goal')) -> f (Maybe (Goals asmp' goal'))
forall a b. f (a -> b) -> f a -> f b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> Goals asmp goal -> f (Maybe (Goals asmp' goal'))
go Goals asmp goal
g2

  assuming' :: (asmp, Maybe (Goals asmp goal)) -> Maybe (Goals asmp goal)
assuming' (asmp
_, Maybe (Goals asmp goal)
Nothing) = Maybe (Goals asmp goal)
forall a. Maybe a
Nothing
  assuming' (asmp
as, Just Goals asmp goal
g) = Goals asmp goal -> Maybe (Goals asmp goal)
forall a. a -> Maybe a
Just (Goals asmp goal -> Maybe (Goals asmp goal))
-> Goals asmp goal -> Maybe (Goals asmp goal)
forall a b. (a -> b) -> a -> b
$! asmp -> Goals asmp goal -> Goals asmp goal
forall asmp goal.
Monoid asmp =>
asmp -> Goals asmp goal -> Goals asmp goal
assuming asmp
as Goals asmp goal
g


traverseOnlyGoals :: (Applicative f, Monoid asmp) =>
  (goal -> f (Maybe goal')) ->
  Goals asmp goal -> f (Maybe (Goals asmp goal'))
traverseOnlyGoals :: forall (f :: Type -> Type) asmp goal goal'.
(Applicative f, Monoid asmp) =>
(goal -> f (Maybe goal'))
-> Goals asmp goal -> f (Maybe (Goals asmp goal'))
traverseOnlyGoals goal -> f (Maybe goal')
f = (forall a. asmp -> f a -> f (asmp, a))
-> (goal -> f (Maybe goal'))
-> Goals asmp goal
-> f (Maybe (Goals asmp goal'))
forall (f :: Type -> Type) asmp' asmp goal goal'.
(Applicative f, Monoid asmp') =>
(forall a. asmp -> f a -> f (asmp', a))
-> (goal -> f (Maybe goal'))
-> Goals asmp goal
-> f (Maybe (Goals asmp' goal'))
traverseGoals (\asmp
as f a
m -> (asmp
as,) (a -> (asmp, a)) -> f a -> f (asmp, a)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> f a
m) goal -> f (Maybe goal')
f

-- | 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.
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'))
traverseGoalsSeq :: forall (f :: Type -> Type) asmp' asmp goal goal'.
(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'))
traverseGoalsSeq forall a. asmp -> f a -> f (asmp', a)
fas goal -> f (Maybe goal')
fgl = Seq (Goals asmp goal) -> f (Seq (Goals asmp' goal'))
go
  where
  go :: Seq (Goals asmp goal) -> f (Seq (Goals asmp' goal'))
go Seq (Goals asmp goal)
Seq.Empty      = Seq (Goals asmp' goal') -> f (Seq (Goals asmp' goal'))
forall a. a -> f a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Seq (Goals asmp' goal')
forall a. Seq a
Seq.Empty
  go (Goals asmp goal
g Seq.:<| Seq (Goals asmp goal)
gs) = Maybe (Goals asmp' goal')
-> Seq (Goals asmp' goal') -> Seq (Goals asmp' goal')
forall {a}. Maybe a -> Seq a -> Seq a
combine (Maybe (Goals asmp' goal')
 -> Seq (Goals asmp' goal') -> Seq (Goals asmp' goal'))
-> f (Maybe (Goals asmp' goal'))
-> f (Seq (Goals asmp' goal') -> Seq (Goals asmp' goal'))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall a. asmp -> f a -> f (asmp', a))
-> (goal -> f (Maybe goal'))
-> Goals asmp goal
-> f (Maybe (Goals asmp' goal'))
forall (f :: Type -> Type) asmp' asmp goal goal'.
(Applicative f, Monoid asmp') =>
(forall a. asmp -> f a -> f (asmp', a))
-> (goal -> f (Maybe goal'))
-> Goals asmp goal
-> f (Maybe (Goals asmp' goal'))
traverseGoals asmp -> f a -> f (asmp', a)
forall a. asmp -> f a -> f (asmp', a)
fas goal -> f (Maybe goal')
fgl Goals asmp goal
g f (Seq (Goals asmp' goal') -> Seq (Goals asmp' goal'))
-> f (Seq (Goals asmp' goal')) -> f (Seq (Goals asmp' goal'))
forall a b. f (a -> b) -> f a -> f b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> Seq (Goals asmp goal) -> f (Seq (Goals asmp' goal'))
go Seq (Goals asmp goal)
gs

  combine :: Maybe a -> Seq a -> Seq a
combine Maybe a
Nothing Seq a
gs  = Seq a
gs
  combine (Just a
g) Seq a
gs = a
g a -> Seq a -> Seq a
forall a. a -> Seq a -> Seq a
Seq.<| Seq a
gs

-- | Visit every goal in a 'Goals' structure, remembering the sequence of
--   assumptions along the way to that goal.
traverseGoalsWithAssumptions :: (Applicative f, Monoid asmp) =>
  (asmp -> goal -> f (Maybe goal')) ->
  Goals asmp goal -> f (Maybe (Goals asmp goal'))

traverseGoalsWithAssumptions :: forall (f :: Type -> Type) asmp goal goal'.
(Applicative f, Monoid asmp) =>
(asmp -> goal -> f (Maybe goal'))
-> Goals asmp goal -> f (Maybe (Goals asmp goal'))
traverseGoalsWithAssumptions asmp -> goal -> f (Maybe goal')
f Goals asmp goal
gls =
   ReaderT asmp f (Maybe (Goals asmp goal'))
-> asmp -> f (Maybe (Goals asmp goal'))
forall r (m :: Type -> Type) a. ReaderT r m a -> r -> m a
runReaderT ((forall a. asmp -> ReaderT asmp f a -> ReaderT asmp f (asmp, a))
-> (goal -> ReaderT asmp f (Maybe goal'))
-> Goals asmp goal
-> ReaderT asmp f (Maybe (Goals asmp goal'))
forall (f :: Type -> Type) asmp' asmp goal goal'.
(Applicative f, Monoid asmp') =>
(forall a. asmp -> f a -> f (asmp', a))
-> (goal -> f (Maybe goal'))
-> Goals asmp goal
-> f (Maybe (Goals asmp' goal'))
traverseGoals asmp -> ReaderT asmp f a -> ReaderT asmp f (asmp, a)
forall a. asmp -> ReaderT asmp f a -> ReaderT asmp f (asmp, a)
forall {m :: Type -> Type} {r} {a}.
(Functor m, Semigroup r) =>
r -> ReaderT r m a -> ReaderT r m (r, a)
fas goal -> ReaderT asmp f (Maybe goal')
fgl Goals asmp goal
gls) asmp
forall a. Monoid a => a
mempty
  where
  fas :: r -> ReaderT r m a -> ReaderT r m (r, a)
fas r
a ReaderT r m a
m = (r
a,) (a -> (r, a)) -> ReaderT r m a -> ReaderT r m (r, a)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (r -> r) -> ReaderT r m a -> ReaderT r m a
forall r' r (m :: Type -> Type) a.
(r' -> r) -> ReaderT r m a -> ReaderT r' m a
withReaderT (r -> r -> r
forall a. Semigroup a => a -> a -> a
<> r
a) ReaderT r m a
m
  fgl :: goal -> ReaderT asmp f (Maybe goal')
fgl goal
gl  = (asmp -> f (Maybe goal')) -> ReaderT asmp f (Maybe goal')
forall r (m :: Type -> Type) a. (r -> m a) -> ReaderT r m a
ReaderT ((asmp -> f (Maybe goal')) -> ReaderT asmp f (Maybe goal'))
-> (asmp -> f (Maybe goal')) -> ReaderT asmp f (Maybe goal')
forall a b. (a -> b) -> a -> b
$ \asmp
as -> asmp -> goal -> f (Maybe goal')
f asmp
as goal
gl