ProofGoals.hs

{-|
Module      : Lang.Crucible.Backend.ProofGoals
Copyright   : (c) Galois, Inc 2014-2018
License     : BSD3

This module defines a data structure ('GoalCollector') for storing the current
state of assumptions and a collection of proof obligations.
-}

{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TupleSections #-}

module Lang.Crucible.Backend.ProofGoals
  ( -- * Goals
    ProofGoal(..), Goals(..), goalsToList, proveAll, goalsConj
    -- ** traversals
  , traverseGoals, traverseOnlyGoals
  , traverseGoalsWithAssumptions
  , traverseGoalsSeq

    -- * Goal collector
  , FrameIdentifier(..), GoalCollector
  , emptyGoalCollector
  , ppGoalCollector

    -- ** traversals
  , traverseGoalCollector
  , traverseGoalCollectorWithAssumptions

    -- ** Context management
  , gcAddAssumes, gcProve
  , gcPush, gcPop, gcAddGoals, gcAddTopLevelAssume,

    -- ** Global operations on context
    gcRemoveObligations, gcRestore, gcReset, gcFinish

    -- ** Viewing the assumption state
  , AssumptionFrames(..), gcFrames
  )
  where

import           Control.Monad.Reader
import qualified Data.Foldable as F
import           Data.Sequence (Seq)
import qualified Data.Sequence as Seq
import           Data.Word (Word64)
import qualified Prettyprinter as PP

import           Lang.Crucible.Backend.Goals

-- | 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.
newtype FrameIdentifier = FrameIdentifier Word64
 deriving(Eq,Ord,Show)


-- | 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
--   'Lang.Crucible.Backend.AssumptionStack.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'.
data GoalCollector asmp goal
  = TopCollector !(Seq (Goals asmp goal))
  | CollectorFrame !FrameIdentifier !(GoalCollector asmp goal)
  | CollectingAssumptions !asmp !(GoalCollector asmp goal)
  | CollectingGoals !(Seq (Goals asmp goal)) !(GoalCollector asmp goal)

ppGoalCollector ::
  forall asmp goal ann.
  (asmp -> PP.Doc ann) ->
  (goal -> PP.Doc ann) ->
  GoalCollector asmp goal ->
  PP.Doc ann
ppGoalCollector ppAsmp ppGoal = go mempty
  where
    go :: PP.Doc ann -> GoalCollector asmp goal -> PP.Doc ann
    go remainder =
      \case
        TopCollector gls ->
          PP.vcat
          [ PP.pretty "Top-level goals:"
          , PP.list (map (ppGoals ppAsmp ppGoal) (F.toList gls))
          , remainder
          ]
        CollectorFrame (FrameIdentifier fid) gc ->
          let pLines = [PP.pretty "Frame " <> PP.viaShow fid <> PP.pretty ":", remainder] in
          go (PP.hang 2 (PP.vcat pLines)) gc
        CollectingAssumptions asmp gc ->
          let pLines = [PP.pretty "Assumptions:" , ppAsmp asmp, remainder] in
          go (PP.hang 2 (PP.vcat pLines)) gc
        CollectingGoals gls gc ->
          let pLines = [ PP.pretty "Prove all:"
                       , PP.list (map (ppGoals ppAsmp ppGoal) (F.toList gls))
                       , remainder
                       ] in
          go (PP.hang 2 (PP.vcat pLines)) gc

-- | Intended for debugging, this is not generally a user-facing datatype.
instance (PP.Pretty asmp, PP.Pretty goal) => PP.Pretty (GoalCollector asmp goal) where
  pretty = ppGoalCollector PP.pretty PP.pretty

-- | A collector with no goals and no context.
emptyGoalCollector :: GoalCollector asmp goal
emptyGoalCollector = TopCollector mempty

-- | Traverse the goals in a 'GoalCollector.  See 'traverseGoals'
--   for an explaination of the action arguments.
traverseGoalCollector :: (Applicative f, Monoid asmp') =>
  (forall a. asmp -> f a -> f (asmp', a)) ->
  (goal -> f (Maybe goal')) ->
  GoalCollector asmp goal -> f (GoalCollector asmp' goal')
traverseGoalCollector fas fgl = go
 where
 go (TopCollector gls) = TopCollector <$> traverseGoalsSeq fas fgl gls
 go (CollectorFrame fid gls) = CollectorFrame fid <$> go gls
 go (CollectingAssumptions asmps gls) = CollectingAssumptions <$> (fst <$> fas asmps (pure ())) <*> go gls
 go (CollectingGoals gs gls) = CollectingGoals <$> traverseGoalsSeq fas fgl gs <*> go gls

-- | Traverse the goals in a 'GoalCollector', keeping track,
--   for each goal, of the assumptions leading to that goal.
traverseGoalCollectorWithAssumptions :: (Applicative f, Monoid asmp) =>
  (asmp -> goal -> f (Maybe goal')) ->
  GoalCollector asmp goal -> f (GoalCollector asmp goal')
traverseGoalCollectorWithAssumptions f gc =
    runReaderT (traverseGoalCollector fas fgl gc) mempty
  where
  fas a m = (a,) <$> withReaderT (<> a) m
  fgl gl  = ReaderT $ \as -> f as gl


-- | The 'AssumptionFrames' data structure captures the current state of
--   assumptions made inside a 'GoalCollector'.
data AssumptionFrames asmp =
  AssumptionFrames
  { -- | Assumptions made at the top level of a solver.
    baseFrame    :: !asmp
    -- | A sequence of pushed frames, together with the assumptions that
    --   were made in each frame.  The sequence is organized with newest
    --   frames on the end (right side) of the sequence.
  , pushedFrames :: !(Seq (FrameIdentifier, asmp))
  }

-- | 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.
gcFrames :: forall asmp goal. Monoid asmp => GoalCollector asmp goal -> AssumptionFrames asmp
gcFrames = go mempty mempty
  where
  go ::
    asmp ->
    Seq (FrameIdentifier, asmp) ->
    GoalCollector asmp goal ->
    AssumptionFrames asmp

  go as fs (TopCollector _)
    = AssumptionFrames as fs

  go as fs (CollectorFrame frmid gc) =
    go mempty ((frmid, as) Seq.<| fs) gc

  go as fs (CollectingAssumptions as' gc) =
    go (as' <> as) fs gc

  go as fs (CollectingGoals _ gc) =
    go as fs gc

-- | Mark the current frame.  Using 'gcPop' will unwind to here.
gcPush :: FrameIdentifier -> GoalCollector asmp goal -> GoalCollector asmp goal
gcPush frmid gc = CollectorFrame frmid gc

gcAddGoals :: Goals asmp goal -> GoalCollector asmp goal -> GoalCollector asmp goal
gcAddGoals g (TopCollector gs) = TopCollector (gs Seq.|> g)
gcAddGoals g (CollectingGoals gs gc) = CollectingGoals (gs Seq.|> g) gc
gcAddGoals g gc = CollectingGoals (Seq.singleton g) gc

-- | Add an assumption that is in scope for all goals, even ones in earlier
-- frames.
gcAddTopLevelAssume ::
  Monoid asmp =>
  asmp ->
  GoalCollector asmp goal ->
  GoalCollector asmp goal
gcAddTopLevelAssume asmp =
  \case
    TopCollector gls ->
      -- Syntactically, it appears that `asmp` is duplicated here, perhaps
      -- unnecessarily. In fact, this is necessary. The `CollectingAssumptions`
      -- constructor brings the assumption into scope for all the goals
      -- *outside* of the top-level (see the comment on `GoalCollector` for
      -- the "inside-out" structure of `GoalCollector`), whereas the `assuming`
      -- brings it into scope for top-level goals.
      CollectingAssumptions asmp (TopCollector (assuming asmp <$> gls))
    CollectorFrame frm gc ->
      CollectorFrame frm (gcAddTopLevelAssume asmp gc)
    CollectingAssumptions asmp' gc ->
      CollectingAssumptions asmp' (gcAddTopLevelAssume asmp gc)
    CollectingGoals gls gc ->
      CollectingGoals gls (gcAddTopLevelAssume asmp gc)

-- | Add a new proof obligation to the current context.
gcProve :: goal -> GoalCollector asmp goal -> GoalCollector asmp goal
gcProve g = gcAddGoals (Prove g)

-- | Add a sequence of extra assumptions to the current context.
gcAddAssumes :: Monoid asmp => asmp -> GoalCollector asmp goal -> GoalCollector asmp goal
gcAddAssumes as' (CollectingAssumptions as gls) = CollectingAssumptions (as <> as') gls
gcAddAssumes as' gls = CollectingAssumptions as' gls

{- | 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. -}

gcPop ::
  Monoid asmp =>
  GoalCollector asmp goal ->
  Either (FrameIdentifier, asmp, Maybe (Goals asmp goal), GoalCollector asmp goal)
         (Maybe (Goals asmp goal))
gcPop = go Nothing mempty
  where

  {- The function `go` completes frames one at a time.  The "hole" is what
     we should use to complete the current path.  If it is 'Nothing', then
     there was nothing interesting on the current path, and we discard
     assumptions that lead to here -}
  go hole _as (TopCollector gs) =
    Right (goalsConj (proveAll gs) hole)

  go hole as (CollectorFrame fid gc) =
    Left (fid, as, hole, gc)

  go hole as (CollectingAssumptions as' gc) =
    go (assuming as' <$> hole) (as' <> as) gc

  go hole as (CollectingGoals gs gc) =
    go (goalsConj (proveAll gs) hole) as gc

-- | Get all currently collected goals.
gcFinish :: Monoid asmp => GoalCollector asmp goal -> Maybe (Goals asmp goal)
gcFinish gc = case gcPop gc of
                Left (_,_,Just g,gc1)  -> gcFinish (gcAddGoals g gc1)
                Left (_,_,Nothing,gc1) -> gcFinish gc1
                Right a -> a

-- | Reset the goal collector to the empty assumption state; but first
--   collect all the pending proof goals and stash them.
gcReset :: Monoid asmp => GoalCollector asmp goal -> GoalCollector asmp goal
gcReset gc = TopCollector gls
  where
  gls = case gcFinish gc of
          Nothing     -> mempty
          Just p      -> Seq.singleton p

pushGoalsToTop :: Goals asmp goal -> GoalCollector asmp goal -> GoalCollector asmp goal
pushGoalsToTop gls = go
 where
 go (TopCollector gls') = TopCollector (gls' Seq.|> gls)
 go (CollectorFrame fid gc) = CollectorFrame fid (go gc)
 go (CollectingAssumptions as gc) = CollectingAssumptions as (go gc)
 go (CollectingGoals gs gc) = CollectingGoals gs (go gc)

-- | 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.
gcRestore ::
  Monoid asmp =>
  GoalCollector asmp goal {- ^ The assumption state to restore -} ->
  GoalCollector asmp goal {- ^ The assumptions state to overwrite -} ->
  GoalCollector asmp goal
gcRestore restore old =
  case gcFinish old of
    Nothing -> restore
    Just p  -> pushGoalsToTop p restore

-- | Remove all collected proof obligations, but keep the current set
-- of assumptions.
gcRemoveObligations :: Monoid asmp => GoalCollector asmp goal -> GoalCollector asmp goal
gcRemoveObligations = go
 where
 go (TopCollector _) = TopCollector mempty
 go (CollectorFrame fid gc) = CollectorFrame fid (go gc)
 go (CollectingAssumptions as gc) =
      case go gc of
        CollectingAssumptions as' gc' -> CollectingAssumptions (as <> as') gc'
        gc' -> CollectingAssumptions as gc'
 go (CollectingGoals _ gc) = go gc