    -----------------------------------------------------------------------------
    -- |
    -- Module    : Data.SBV.Tools.WeakestPreconditions
    -- Copyright : (c) Levent Erkok
    -- License   : BSD3
    -- Maintainer: erkokl@gmail.com
    -- Stability : experimental
    --
    -- A toy imperative language with a proof system based on Dijkstra's weakest
    -- preconditions methodology to establish partial/total correctness proofs.
    --
    -- See @Documentation.SBV.Examples.WeakestPreconditions@ directory for
    -- several example proofs.
    -----------------------------------------------------------------------------

    {-# LANGUAGE FlexibleContexts       #-}
    {-# LANGUAGE MultiParamTypeClasses  #-}
    {-# LANGUAGE NamedFieldPuns         #-}
    {-# LANGUAGE ScopedTypeVariables    #-}
    {-# LANGUAGE TypeFamilies           #-}
    {-# LANGUAGE TypeOperators          #-}

    {-# OPTIONS_GHC -Wall -Werror #-}

    module Data.SBV.Tools.WeakestPreconditions (
            -- * Programs and statements
              Program(..), Stmt(..), assert, stable

            -- * Invariants, measures, and stability
            , Invariant, Measure, Stable

            -- * Verification conditions
            , VC(..)

            -- * Result of a proof
            , ProofResult(..)

            -- * Configuring the WP engine
            , WPConfig(..), defaultWPCfg

            -- * Checking WP correctness
            , wpProve, wpProveWith

            -- * Concrete runs of programs
            , traceExecution, Status(..)
            ) where

    import Data.List   (intercalate)
    import Data.Maybe  (fromJust, isJust, isNothing)

    import Control.Monad (when)

    import Data.SBV
    import Data.SBV.Control

    -- | A program over a state is simply a statement, together with
    -- a pre-condition capturing environmental assumptions and
    -- a post-condition that states its correctness. In the usual
    -- Hoare-triple notation, it captures:
    --
    --   @ {precondition} program {postcondition} @
    --
    -- We also allow for a stability check, which is ensured at
    -- every assignment statement to deal with ghost variables.
    -- In general, this is useful for making sure what you consider
    -- as "primary inputs" remain unaffected. Of course, you can
    -- also put any arbitrary condition you want to check that you
    -- want performed for each 'Assign' statement.
    --
    -- Note that stability is quite a strong condition: It is intended
    -- to capture constants that never change during execution. So,
    -- if you have a program that changes an input temporarily but
    -- always restores it at the end, it would still fail the stability
    -- condition.
    --
    -- The 'setup' field is reserved for any symbolic code you might
    -- want to run before the proof takes place, typically for calls
    -- to 'Data.SBV.setOption'. If not needed, simply pass @return ()@.
    -- For an interesting use case where we use setup to axiomatize
    -- the spec, see "Documentation.SBV.Examples.WeakestPreconditions.Fib"
    -- and "Documentation.SBV.Examples.WeakestPreconditions.GCD".
    data Program st = Program { forall st. Program st -> Symbolic ()
    setup         :: Symbolic ()  -- ^ Any set-up required
                              , forall st. Program st -> st -> SBool
    precondition  :: st -> SBool  -- ^ Environmental assumptions
                              , forall st. Program st -> Stmt st
    program       :: Stmt st      -- ^ Program
                              , forall st. Program st -> st -> SBool
    postcondition :: st -> SBool  -- ^ Correctness statement
                              , forall st. Program st -> Stable st
    stability     :: Stable st    -- ^ Each assignment must satisfy stability
                              }

    -- | A stability condition captures a primary input that does not change. Use 'stable'
    -- to create elements of this type.
    type Stable st = [st -> st -> (String, SBool)]

    -- | An invariant takes a state and evaluates to a boolean.
    type Invariant st = st -> SBool

    -- | A measure takes the state and returns a sequence of integers. The ordering
    -- will be done lexicographically over the elements.
    type Measure st = st -> [SInteger]

    -- | A statement in our imperative program, parameterized over the state.
    data Stmt st = Skip                                                                     -- ^ Skip, do nothing.
                 | Abort String                                                             -- ^ Abort execution. The name is for diagnostic purposes.
                 | Assign (st -> st)                                                        -- ^ Assignment: Transform the state by a function.
                 | If (st -> SBool) (Stmt st) (Stmt st)                                     -- ^ Conditional: @If condition thenBranch elseBranch@.
                 | While String (Invariant st) (Maybe (Measure st)) (st -> SBool) (Stmt st) -- ^ A while loop: @While name invariant measure condition body@.
                                                                                            -- The string @name@ is merely for diagnostic purposes.
                                                                                            -- If the measure is 'Nothing', then only partial correctness
                                                                                            -- of this loop will be proven.
                 | Seq [Stmt st]                                                            -- ^ A sequence of statements.

    -- | An 'assert' is a quick way of ensuring some condition holds. If it does,
    -- then it's equivalent to 'Skip'. Otherwise, it is equivalent to 'Abort'.
    assert :: String -> (st -> SBool) -> Stmt st
    assert :: forall st. String -> (st -> SBool) -> Stmt st
    assert String
    nm st -> SBool
    cond = (st -> SBool) -> Stmt st -> Stmt st -> Stmt st
    forall st. (st -> SBool) -> Stmt st -> Stmt st -> Stmt st
    If st -> SBool
    cond Stmt st
    forall st. Stmt st
    Skip (String -> Stmt st
    forall st. String -> Stmt st
    Abort String
    nm)

    -- | Stability: A call of the form @stable "f" f@ means the value of the field @f@
    -- does not change during any assignment. The string argument is for diagnostic
    -- purposes only. Note that we use strong-equality here, so if the program
    -- is manipulating floats, we don't get a false-positive on @NaN@ and also
    -- not miss @+0@ and @-@@ changes.
    stable :: EqSymbolic a => String -> (st -> a) -> st -> st -> (String, SBool)
    stable :: forall a st.
    EqSymbolic a =>
    String -> (st -> a) -> st -> st -> (String, SBool)
    stable String
    nm st -> a
    f st
    before st
    after = (String
    nm, st -> a
    f st
    before a -> a -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .=== st -> a
    f st
    after)

    -- | Are all the termination measures provided?
    isTotal :: Stmt st -> Bool
    isTotal :: forall st. Stmt st -> Bool
    isTotal Stmt st
    Skip                = Bool
    True
    isTotal (Abort String
    _)           = Bool
    True
    isTotal (Assign st -> st
    _)          = Bool
    True
    isTotal (If st -> SBool
    _ Stmt st
    tb Stmt st
    fb)        = (Stmt st -> Bool) -> [Stmt st] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    all Stmt st -> Bool
    forall st. Stmt st -> Bool
    isTotal [Stmt st
    tb, Stmt st
    fb]
    isTotal (While String
    _ st -> SBool
    _ Maybe (Measure st)
    msr st -> SBool
    _ Stmt st
    s) = Maybe (Measure st) -> Bool
    forall a. Maybe a -> Bool
    isJust Maybe (Measure st)
    msr Bool -> Bool -> Bool
    && Stmt st -> Bool
    forall st. Stmt st -> Bool
    isTotal Stmt st
    s
    isTotal (Seq [Stmt st]
    ss)            = (Stmt st -> Bool) -> [Stmt st] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    all Stmt st -> Bool
    forall st. Stmt st -> Bool
    isTotal [Stmt st]
    ss

    -- | A verification condition. Upon failure, each 'VC' carries enough state and diagnostic information
    -- to indicate what particular proof obligation failed for further debugging.
    data VC st m = BadPrecondition          st                  -- ^ The precondition doesn't hold. This can only happen in 'traceExecution'.
                 | BadPostcondition         st st               -- ^ The postcondition doesn't hold
                 | Unstable          String st st               -- ^ Stability condition is violated
                 | AbortReachable    String st st               -- ^ The named abort condition is reachable
                 | InvariantPre      String st                  -- ^ Invariant doesn't hold upon entry to the named loop
                 | InvariantMaintain String st st               -- ^ Invariant isn't maintained by the body
                 | MeasureBound      String (st, [m])           -- ^ Measure cannot be shown to be non-negative
                 | MeasureDecrease   String (st, [m]) (st, [m]) -- ^ Measure cannot be shown to decrease through each iteration

    -- | Helper function to display VC's nicely
    dispVC :: String -> [(String, String)] -> String
    dispVC :: String -> [(String, String)] -> String
    dispVC String
    tag [(String, String)]
    flds = String -> [String] -> String
    forall a. [a] -> [[a]] -> [a]
    intercalate String
    "\n" ([String] -> String) -> [String] -> String
    forall a b. (a -> b) -> a -> b
    $ String -> String
    col String
    tag String -> [String] -> [String]
    forall a. a -> [a] -> [a]
    : ((String, String) -> String) -> [(String, String)] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map (String, String) -> String
    showField [(String, String)]
    flds
      where col :: String -> String
    col String
    "" = String
    ""
            col String
    t  = String
    t String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ":"

            showField :: (String, String) -> String
    showField (String
    t, String
    c) = String -> [String] -> String
    forall a. [a] -> [[a]] -> [a]
    intercalate String
    "\n" ([String] -> String) -> [String] -> String
    forall a b. (a -> b) -> a -> b
    $ (Int -> String -> String) -> [Int] -> [String] -> [String]
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith Int -> String -> String
    mark [(Int
    1::Int)..] (String -> [String]
    lines String
    c)
               where tt :: String
    tt   = if String -> Bool
    forall a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null String
    t then String
    "" else String -> String
    col String
    t String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " "
                     sp :: String
    sp   = Int -> Char -> String
    forall a. Int -> a -> [a]
    replicate (String -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length String
    tt) Char
    ' '
                     mark :: Int -> String -> String
    mark Int
    i String
    s = String
    "  " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ (if Int
    i Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == Int
    1 then String
    tt else String
    sp) String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    s

    -- If a measure is a singleton, just show the number. Otherwise as a list:
    showMeasure :: Show a => [a] -> String
    showMeasure :: forall a. Show a => [a] -> String
    showMeasure [a
    x] = a -> String
    forall a. Show a => a -> String
    show a
    x
    showMeasure [a]
    xs  = [a] -> String
    forall a. Show a => a -> String
    show [a]
    xs

    -- | Show instance for VC's
    instance (Show st, Show m) => Show (VC st m) where
      show :: VC st m -> String
    show (BadPrecondition   st
    s)                    = String -> [(String, String)] -> String
    dispVC String
    "Precondition fails"
                                                             [(String
    "", st -> String
    forall a. Show a => a -> String
    show st
    s)]
      show (BadPostcondition  st
    s1 st
    s2)                = String -> [(String, String)] -> String
    dispVC String
    "Postcondition fails"
                                                             [ (String
    "Start", st -> String
    forall a. Show a => a -> String
    show st
    s1)
                                                             , (String
    "End  ", st -> String
    forall a. Show a => a -> String
    show st
    s2)
                                                             ]
      show (Unstable          String
    m st
    s1 st
    s2)              = String -> [(String, String)] -> String
    dispVC (String
    "Stability fails for " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String -> String
    forall a. Show a => a -> String
    show String
    m)
                                                             [ (String
    "Before", st -> String
    forall a. Show a => a -> String
    show st
    s1)
                                                             , (String
    "After ", st -> String
    forall a. Show a => a -> String
    show st
    s2)
                                                             ]
      show (AbortReachable    String
    nm st
    s1 st
    s2)             = String -> [(String, String)] -> String
    dispVC (String
    "Abort " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String -> String
    forall a. Show a => a -> String
    show String
    nm String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " condition is satisfiable")
                                                             [ (String
    "Before", st -> String
    forall a. Show a => a -> String
    show st
    s1)
                                                             , (String
    "After ", st -> String
    forall a. Show a => a -> String
    show st
    s2)
                                                             ]
      show (InvariantPre      String
    nm st
    s)                 = String -> [(String, String)] -> String
    dispVC (String
    "Invariant for loop " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String -> String
    forall a. Show a => a -> String
    show String
    nm String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " fails upon entry")
                                                             [(String
    "", st -> String
    forall a. Show a => a -> String
    show st
    s)]
      show (InvariantMaintain String
    nm st
    s1 st
    s2)             = String -> [(String, String)] -> String
    dispVC (String
    "Invariant for loop " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String -> String
    forall a. Show a => a -> String
    show String
    nm String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " is not maintained by the body")
                                                             [ (String
    "Before", st -> String
    forall a. Show a => a -> String
    show st
    s1)
                                                             , (String
    "After ", st -> String
    forall a. Show a => a -> String
    show st
    s2)
                                                             ]
      show (MeasureBound      String
    nm (st
    s, [m]
    m))            = String -> [(String, String)] -> String
    dispVC (String
    "Measure for loop "   String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String -> String
    forall a. Show a => a -> String
    show String
    nm String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " is negative")
                                                             [ (String
    "State  ", st -> String
    forall a. Show a => a -> String
    show st
    s)
                                                             , (String
    "Measure", [m] -> String
    forall a. Show a => [a] -> String
    showMeasure [m]
    m )
                                                             ]
      show (MeasureDecrease   String
    nm (st
    s1, [m]
    m1) (st
    s2, [m]
    m2)) = String -> [(String, String)] -> String
    dispVC (String
    "Measure for loop "   String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String -> String
    forall a. Show a => a -> String
    show String
    nm String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " does not decrease")
                                                             [ (String
    "Before ", st -> String
    forall a. Show a => a -> String
    show st
    s1)
                                                             , (String
    "Measure", [m] -> String
    forall a. Show a => [a] -> String
    showMeasure [m]
    m1)
                                                             , (String
    "After  ", st -> String
    forall a. Show a => a -> String
    show st
    s2)
                                                             , (String
    "Measure", [m] -> String
    forall a. Show a => [a] -> String
    showMeasure [m]
    m2)
                                                             ]

    -- | The result of a weakest-precondition proof.
    data ProofResult res = Proven Bool                -- ^ The property holds. If 'Bool' is 'True', then total correctness, otherwise partial.
                         | Indeterminate String       -- ^ Failed to establish correctness. Happens when the proof obligations lead to
                                                      -- the SMT solver to return @Unk@. This can happen, for instance, if you have
                                                      -- non-linear constraints, causing the solver to give up.
                         | Failed [VC res Integer]    -- ^ The property fails, failing to establish the conditions listed.

    -- | 'Show' instance for proofs, for readability.
    instance Show res => Show (ProofResult res) where
      show :: ProofResult res -> String
    show (Proven Bool
    True)     = String
    "Q.E.D."
      show (Proven Bool
    False)    = String
    "Q.E.D. [Partial: not all termination measures were provided.]"
      show (Indeterminate String
    s) = String
    "Indeterminate: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    s
      show (Failed [VC res Integer]
    vcs)      = String -> [String] -> String
    forall a. [a] -> [[a]] -> [a]
    intercalate String
    "\n" ([String] -> String) -> [String] -> String
    forall a b. (a -> b) -> a -> b
    $ (String
    "Proof failure. Failing verification condition" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ if [VC res Integer] -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [VC res Integer]
    vcs Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    > Int
    1 then String
    "s:" else String
    ":")
                                                  String -> [String] -> [String]
    forall a. a -> [a] -> [a]
    : (VC res Integer -> String) -> [VC res Integer] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map (\VC res Integer
    vc -> String -> [String] -> String
    forall a. [a] -> [[a]] -> [a]
    intercalate String
    "\n" [String
    "  " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    l | String
    l <- String -> [String]
    lines (VC res Integer -> String
    forall a. Show a => a -> String
    show VC res Integer
    vc)]) [VC res Integer]
    vcs

    -- | Checking WP based correctness
    wpProveWith :: forall st res. (Show res, Mergeable st, Queriable IO st, res ~ QueryResult st) => WPConfig -> Program st -> IO (ProofResult res)
    wpProveWith :: forall st res.
    (Show res, Mergeable st, Queriable IO st, res ~ QueryResult st) =>
    WPConfig -> Program st -> IO (ProofResult res)
    wpProveWith cfg :: WPConfig
    cfg@WPConfig{Bool
    wpVerbose :: Bool
    wpVerbose :: WPConfig -> Bool
    wpVerbose} Program{Symbolic ()
    setup :: forall st. Program st -> Symbolic ()
    setup :: Symbolic ()
    setup, st -> SBool
    precondition :: forall st. Program st -> st -> SBool
    precondition :: st -> SBool
    precondition, Stmt st
    program :: forall st. Program st -> Stmt st
    program :: Stmt st
    program, st -> SBool
    postcondition :: forall st. Program st -> st -> SBool
    postcondition :: st -> SBool
    postcondition, Stable st
    stability :: forall st. Program st -> Stable st
    stability :: Stable st
    stability} =
       SMTConfig -> Symbolic (ProofResult res) -> IO (ProofResult res)
    forall a. SMTConfig -> Symbolic a -> IO a
    runSMTWith (WPConfig -> SMTConfig
    wpSolver WPConfig
    cfg) (Symbolic (ProofResult res) -> IO (ProofResult res))
    -> Symbolic (ProofResult res) -> IO (ProofResult res)
    forall a b. (a -> b) -> a -> b
    $ do Symbolic ()
    setup
                                      Query (ProofResult res) -> Symbolic (ProofResult res)
    forall a. Query a -> Symbolic a
    query Query (ProofResult res)
    q
      where q :: Query (ProofResult res)
    q = do st
    start <- QueryT IO st
    forall (m :: * -> *) a. Queriable m a => QueryT m a
    create

                   st -> [(SBool, VC st SInteger)]
    weakestPrecondition <- st
    -> Stmt st
    -> (st -> [(SBool, VC st SInteger)])
    -> Query (st -> [(SBool, VC st SInteger)])
    wp st
    start Stmt st
    program (\st
    st -> [(st -> SBool
    postcondition st
    st, st -> st -> VC st SInteger
    forall st m. st -> st -> VC st m
    BadPostcondition st
    start st
    st)])

                   let vcs :: [(SBool, VC st SInteger)]
    vcs = st -> [(SBool, VC st SInteger)]
    weakestPrecondition st
    start

                   SBool -> QueryT IO ()
    forall a. QuantifiedBool a => a -> QueryT IO ()
    forall (m :: * -> *) a.
    (SolverContext m, QuantifiedBool a) =>
    a -> m ()
    constrain (SBool -> QueryT IO ()) -> SBool -> QueryT IO ()
    forall a b. (a -> b) -> a -> b
    $ SBool -> SBool
    sNot (SBool -> SBool) -> SBool -> SBool
    forall a b. (a -> b) -> a -> b
    $ st -> SBool
    precondition st
    start SBool -> SBool -> SBool
    .=> [SBool] -> SBool
    sAnd (((SBool, VC st SInteger) -> SBool)
    -> [(SBool, VC st SInteger)] -> [SBool]
    forall a b. (a -> b) -> [a] -> [b]
    map (SBool, VC st SInteger) -> SBool
    forall a b. (a, b) -> a
    fst [(SBool, VC st SInteger)]
    vcs)

                   CheckSatResult
    cs <- Query CheckSatResult
    checkSat
                   case CheckSatResult
    cs of
                     CheckSatResult
    Unk    -> String -> ProofResult res
    forall res. String -> ProofResult res
    Indeterminate (String -> ProofResult res)
    -> (SMTReasonUnknown -> String)
    -> SMTReasonUnknown
    -> ProofResult res
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . SMTReasonUnknown -> String
    forall a. Show a => a -> String
    show (SMTReasonUnknown -> ProofResult res)
    -> QueryT IO SMTReasonUnknown -> Query (ProofResult res)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QueryT IO SMTReasonUnknown
    getUnknownReason

                     CheckSatResult
    Unsat  -> do let t :: Bool
    t = Stmt st -> Bool
    forall st. Stmt st -> Bool
    isTotal Stmt st
    program

                                  if Bool
    t then String -> QueryT IO ()
    msg String
    "Total correctness is established."
                                       else String -> QueryT IO ()
    msg String
    "Partial correctness is established."

                                  ProofResult res -> Query (ProofResult res)
    forall a. a -> QueryT IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (ProofResult res -> Query (ProofResult res))
    -> ProofResult res -> Query (ProofResult res)
    forall a b. (a -> b) -> a -> b
    $ Bool -> ProofResult res
    forall res. Bool -> ProofResult res
    Proven Bool
    t

                     DSat{} -> ProofResult res -> Query (ProofResult res)
    forall a. a -> QueryT IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (ProofResult res -> Query (ProofResult res))
    -> ProofResult res -> Query (ProofResult res)
    forall a b. (a -> b) -> a -> b
    $ String -> ProofResult res
    forall res. String -> ProofResult res
    Indeterminate String
    "Unsupported: Solver returned a delta-satisfiable answer."

                     CheckSatResult
    Sat    -> do let checkVC :: (SBool, VC st SInteger) -> Query [VC res Integer]
                                      checkVC :: (SBool, VC st SInteger) -> Query [VC res Integer]
    checkVC (SBool
    cond, VC st SInteger
    vc) = do Bool
    c <- SBool -> Query Bool
    forall a. SymVal a => SBV a -> Query a
    getValue SBool
    cond
                                                              if Bool
    c
                                                                 then [VC res Integer] -> Query [VC res Integer]
    forall a. a -> QueryT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return []   -- The VC was OK
                                                                 else do VC res Integer
    vc' <- case VC st SInteger
    vc of
                                                                                  BadPrecondition     st
    s                 -> res -> VC res Integer
    forall st m. st -> VC st m
    BadPrecondition     (res -> VC res Integer)
    -> QueryT IO res -> QueryT IO (VC res Integer)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> st -> QueryT IO (QueryResult st)
    forall (m :: * -> *) a.
    Queriable m a =>
    a -> QueryT m (QueryResult a)
    project st
    s
                                                                                  BadPostcondition    st
    s1 st
    s2             -> res -> res -> VC res Integer
    forall st m. st -> st -> VC st m
    BadPostcondition    (res -> res -> VC res Integer)
    -> QueryT IO res -> QueryT IO (res -> VC res Integer)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> st -> QueryT IO (QueryResult st)
    forall (m :: * -> *) a.
    Queriable m a =>
    a -> QueryT m (QueryResult a)
    project st
    s1 QueryT IO (res -> VC res Integer)
    -> QueryT IO res -> QueryT IO (VC res Integer)
    forall a b. QueryT IO (a -> b) -> QueryT IO a -> QueryT IO b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> st -> QueryT IO (QueryResult st)
    forall (m :: * -> *) a.
    Queriable m a =>
    a -> QueryT m (QueryResult a)
    project st
    s2
                                                                                  Unstable          String
    l st
    s1 st
    s2             -> String -> res -> res -> VC res Integer
    forall st m. String -> st -> st -> VC st m
    Unstable          String
    l (res -> res -> VC res Integer)
    -> QueryT IO res -> QueryT IO (res -> VC res Integer)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> st -> QueryT IO (QueryResult st)
    forall (m :: * -> *) a.
    Queriable m a =>
    a -> QueryT m (QueryResult a)
    project st
    s1 QueryT IO (res -> VC res Integer)
    -> QueryT IO res -> QueryT IO (VC res Integer)
    forall a b. QueryT IO (a -> b) -> QueryT IO a -> QueryT IO b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> st -> QueryT IO (QueryResult st)
    forall (m :: * -> *) a.
    Queriable m a =>
    a -> QueryT m (QueryResult a)
    project st
    s2
                                                                                  AbortReachable    String
    l st
    s1 st
    s2             -> String -> res -> res -> VC res Integer
    forall st m. String -> st -> st -> VC st m
    AbortReachable    String
    l (res -> res -> VC res Integer)
    -> QueryT IO res -> QueryT IO (res -> VC res Integer)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> st -> QueryT IO (QueryResult st)
    forall (m :: * -> *) a.
    Queriable m a =>
    a -> QueryT m (QueryResult a)
    project st
    s1 QueryT IO (res -> VC res Integer)
    -> QueryT IO res -> QueryT IO (VC res Integer)
    forall a b. QueryT IO (a -> b) -> QueryT IO a -> QueryT IO b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> st -> QueryT IO (QueryResult st)
    forall (m :: * -> *) a.
    Queriable m a =>
    a -> QueryT m (QueryResult a)
    project st
    s2
                                                                                  InvariantPre      String
    l st
    s                 -> String -> res -> VC res Integer
    forall st m. String -> st -> VC st m
    InvariantPre      String
    l (res -> VC res Integer)
    -> QueryT IO res -> QueryT IO (VC res Integer)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> st -> QueryT IO (QueryResult st)
    forall (m :: * -> *) a.
    Queriable m a =>
    a -> QueryT m (QueryResult a)
    project st
    s
                                                                                  InvariantMaintain String
    l st
    s1 st
    s2             -> String -> res -> res -> VC res Integer
    forall st m. String -> st -> st -> VC st m
    InvariantMaintain String
    l (res -> res -> VC res Integer)
    -> QueryT IO res -> QueryT IO (res -> VC res Integer)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> st -> QueryT IO (QueryResult st)
    forall (m :: * -> *) a.
    Queriable m a =>
    a -> QueryT m (QueryResult a)
    project st
    s1 QueryT IO (res -> VC res Integer)
    -> QueryT IO res -> QueryT IO (VC res Integer)
    forall a b. QueryT IO (a -> b) -> QueryT IO a -> QueryT IO b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> st -> QueryT IO (QueryResult st)
    forall (m :: * -> *) a.
    Queriable m a =>
    a -> QueryT m (QueryResult a)
    project st
    s2
                                                                                  MeasureBound      String
    l (st
    s, [SInteger]
    m)            -> do res
    r <- st -> QueryT IO (QueryResult st)
    forall (m :: * -> *) a.
    Queriable m a =>
    a -> QueryT m (QueryResult a)
    project st
    s
                                                                                                                              [Integer]
    v <- (SInteger -> QueryT IO Integer)
    -> [SInteger] -> QueryT IO [Integer]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM SInteger -> QueryT IO Integer
    forall a. SymVal a => SBV a -> Query a
    getValue [SInteger]
    m
                                                                                                                              VC res Integer -> QueryT IO (VC res Integer)
    forall a. a -> QueryT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (VC res Integer -> QueryT IO (VC res Integer))
    -> VC res Integer -> QueryT IO (VC res Integer)
    forall a b. (a -> b) -> a -> b
    $ String -> (res, [Integer]) -> VC res Integer
    forall st m. String -> (st, [m]) -> VC st m
    MeasureBound String
    l (res
    r, [Integer]
    v)
                                                                                  MeasureDecrease   String
    l (st
    s1, [SInteger]
    i1) (st
    s2, [SInteger]
    i2) -> do res
    r1 <- st -> QueryT IO (QueryResult st)
    forall (m :: * -> *) a.
    Queriable m a =>
    a -> QueryT m (QueryResult a)
    project st
    s1
                                                                                                                              [Integer]
    v1 <- (SInteger -> QueryT IO Integer)
    -> [SInteger] -> QueryT IO [Integer]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM SInteger -> QueryT IO Integer
    forall a. SymVal a => SBV a -> Query a
    getValue [SInteger]
    i1
                                                                                                                              res
    r2 <- st -> QueryT IO (QueryResult st)
    forall (m :: * -> *) a.
    Queriable m a =>
    a -> QueryT m (QueryResult a)
    project st
    s2
                                                                                                                              [Integer]
    v2 <- (SInteger -> QueryT IO Integer)
    -> [SInteger] -> QueryT IO [Integer]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM SInteger -> QueryT IO Integer
    forall a. SymVal a => SBV a -> Query a
    getValue [SInteger]
    i2
                                                                                                                              VC res Integer -> QueryT IO (VC res Integer)
    forall a. a -> QueryT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (VC res Integer -> QueryT IO (VC res Integer))
    -> VC res Integer -> QueryT IO (VC res Integer)
    forall a b. (a -> b) -> a -> b
    $ String -> (res, [Integer]) -> (res, [Integer]) -> VC res Integer
    forall st m. String -> (st, [m]) -> (st, [m]) -> VC st m
    MeasureDecrease String
    l (res
    r1, [Integer]
    v1) (res
    r2, [Integer]
    v2)
                                                                         [VC res Integer] -> Query [VC res Integer]
    forall a. a -> QueryT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return [VC res Integer
    vc']

                                  [VC res Integer]
    badVCs <- [[VC res Integer]] -> [VC res Integer]
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat ([[VC res Integer]] -> [VC res Integer])
    -> QueryT IO [[VC res Integer]] -> Query [VC res Integer]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ((SBool, VC st SInteger) -> Query [VC res Integer])
    -> [(SBool, VC st SInteger)] -> QueryT IO [[VC res Integer]]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM (SBool, VC st SInteger) -> Query [VC res Integer]
    checkVC [(SBool, VC st SInteger)]
    vcs

                                  Bool -> QueryT IO () -> QueryT IO ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    when ([VC res Integer] -> Bool
    forall a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [VC res Integer]
    badVCs) (QueryT IO () -> QueryT IO ()) -> QueryT IO () -> QueryT IO ()
    forall a b. (a -> b) -> a -> b
    $ String -> QueryT IO ()
    forall a. HasCallStack => String -> a
    error String
    "Data.SBV.proveWP: Impossible happened. Proof failed, but no failing VC found!"

                                  let plu :: String -> [a] -> String
    plu String
    w (a
    _:a
    _:[a]
    _) = String
    w String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "s"
                                      plu String
    w [a]
    _       = String
    w

                                      m :: String
    m = String
    "Following proof " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String -> [VC res Integer] -> String
    forall {a}. String -> [a] -> String
    plu String
    "obligation" [VC res Integer]
    badVCs String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " failed:"

                                  String -> QueryT IO ()
    msg String
    m
                                  String -> QueryT IO ()
    msg (String -> QueryT IO ()) -> String -> QueryT IO ()
    forall a b. (a -> b) -> a -> b
    $ Int -> Char -> String
    forall a. Int -> a -> [a]
    replicate (String -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length String
    m) Char
    '='

                                  let disp :: VC res Integer -> QueryT IO ()
    disp VC res Integer
    c = (String -> QueryT IO ()) -> [String] -> QueryT IO ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ String -> QueryT IO ()
    msg [String
    "  " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    l | String
    l <- String -> [String]
    lines (VC res Integer -> String
    forall a. Show a => a -> String
    show VC res Integer
    c)]
                                  (VC res Integer -> QueryT IO ())
    -> [VC res Integer] -> QueryT IO ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ VC res Integer -> QueryT IO ()
    disp [VC res Integer]
    badVCs

                                  ProofResult res -> Query (ProofResult res)
    forall a. a -> QueryT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (ProofResult res -> Query (ProofResult res))
    -> ProofResult res -> Query (ProofResult res)
    forall a b. (a -> b) -> a -> b
    $ [VC res Integer] -> ProofResult res
    forall res. [VC res Integer] -> ProofResult res
    Failed [VC res Integer]
    badVCs

            msg :: String -> QueryT IO ()
    msg = IO () -> QueryT IO ()
    forall a. IO a -> Query a
    io (IO () -> QueryT IO ())
    -> (String -> IO ()) -> String -> QueryT IO ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Bool -> IO () -> IO ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    when Bool
    wpVerbose (IO () -> IO ()) -> (String -> IO ()) -> String -> IO ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . String -> IO ()
    putStrLn

            -- Compute the weakest precondition to establish the property:
            wp :: st -> Stmt st -> (st -> [(SBool, VC st SInteger)]) -> Query (st -> [(SBool, VC st SInteger)])

            -- Skip simply keeps the conditions
            wp :: st
    -> Stmt st
    -> (st -> [(SBool, VC st SInteger)])
    -> Query (st -> [(SBool, VC st SInteger)])
    wp st
    _ Stmt st
    Skip st -> [(SBool, VC st SInteger)]
    post = (st -> [(SBool, VC st SInteger)])
    -> Query (st -> [(SBool, VC st SInteger)])
    forall a. a -> QueryT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return st -> [(SBool, VC st SInteger)]
    post

            -- Abort is never satisfiable. The only way to have Abort's VC to pass is
            -- to run it in a precondition (either via program or in an if branch) that
            -- evaluates to false, i.e., it must not be reachable.
            wp st
    start (Abort String
    nm) st -> [(SBool, VC st SInteger)]
    _ = (st -> [(SBool, VC st SInteger)])
    -> Query (st -> [(SBool, VC st SInteger)])
    forall a. a -> QueryT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ((st -> [(SBool, VC st SInteger)])
     -> Query (st -> [(SBool, VC st SInteger)]))
    -> (st -> [(SBool, VC st SInteger)])
    -> Query (st -> [(SBool, VC st SInteger)])
    forall a b. (a -> b) -> a -> b
    $ \st
    st -> [(SBool
    sFalse, String -> st -> st -> VC st SInteger
    forall st m. String -> st -> st -> VC st m
    AbortReachable String
    nm st
    start st
    st)]

            -- Assign simply transforms the state and passes on. It also checks that the
            -- stability constraints are not violated.
            wp st
    _ (Assign st -> st
    f) st -> [(SBool, VC st SInteger)]
    post = (st -> [(SBool, VC st SInteger)])
    -> Query (st -> [(SBool, VC st SInteger)])
    forall a. a -> QueryT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ((st -> [(SBool, VC st SInteger)])
     -> Query (st -> [(SBool, VC st SInteger)]))
    -> (st -> [(SBool, VC st SInteger)])
    -> Query (st -> [(SBool, VC st SInteger)])
    forall a b. (a -> b) -> a -> b
    $ \st
    st -> let st' :: st
    st'       = st -> st
    f st
    st
                                                       vcs :: [(SBool, VC st SInteger)]
    vcs       = ((st -> st -> (String, SBool)) -> (SBool, VC st SInteger))
    -> Stable st -> [(SBool, VC st SInteger)]
    forall a b. (a -> b) -> [a] -> [b]
    map (\st -> st -> (String, SBool)
    s -> let (String
    nm, SBool
    b) = st -> st -> (String, SBool)
    s st
    st st
    st' in (SBool
    b, String -> st -> st -> VC st SInteger
    forall st m. String -> st -> st -> VC st m
    Unstable String
    nm st
    st st
    st')) Stable st
    stability
                                                   in [(SBool, VC st SInteger)]
    vcs [(SBool, VC st SInteger)]
    -> [(SBool, VC st SInteger)] -> [(SBool, VC st SInteger)]
    forall a. [a] -> [a] -> [a]
    ++ st -> [(SBool, VC st SInteger)]
    post st
    st'

            -- Conditional: We separately collect the VCs, and predicate with the proper branch condition
            wp st
    start (If st -> SBool
    c Stmt st
    tb Stmt st
    fb) st -> [(SBool, VC st SInteger)]
    post = do st -> [(SBool, VC st SInteger)]
    tWP <- st
    -> Stmt st
    -> (st -> [(SBool, VC st SInteger)])
    -> Query (st -> [(SBool, VC st SInteger)])
    wp st
    start Stmt st
    tb st -> [(SBool, VC st SInteger)]
    post
                                            st -> [(SBool, VC st SInteger)]
    fWP <- st
    -> Stmt st
    -> (st -> [(SBool, VC st SInteger)])
    -> Query (st -> [(SBool, VC st SInteger)])
    wp st
    start Stmt st
    fb st -> [(SBool, VC st SInteger)]
    post
                                            (st -> [(SBool, VC st SInteger)])
    -> Query (st -> [(SBool, VC st SInteger)])
    forall a. a -> QueryT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ((st -> [(SBool, VC st SInteger)])
     -> Query (st -> [(SBool, VC st SInteger)]))
    -> (st -> [(SBool, VC st SInteger)])
    -> Query (st -> [(SBool, VC st SInteger)])
    forall a b. (a -> b) -> a -> b
    $ \st
    st -> let cond :: SBool
    cond = st -> SBool
    c st
    st
                                                            in   [(     SBool
    cond SBool -> SBool -> SBool
    .=> SBool
    b, VC st SInteger
    v) | (SBool
    b, VC st SInteger
    v) <- st -> [(SBool, VC st SInteger)]
    tWP st
    st]
                                                              [(SBool, VC st SInteger)]
    -> [(SBool, VC st SInteger)] -> [(SBool, VC st SInteger)]
    forall a. [a] -> [a] -> [a]
    ++ [(SBool -> SBool
    sNot SBool
    cond SBool -> SBool -> SBool
    .=> SBool
    b, VC st SInteger
    v) | (SBool
    b, VC st SInteger
    v) <- st -> [(SBool, VC st SInteger)]
    fWP st
    st]

            -- Sequencing: Simply run through the statements
            wp st
    _     (Seq [])              st -> [(SBool, VC st SInteger)]
    post = (st -> [(SBool, VC st SInteger)])
    -> Query (st -> [(SBool, VC st SInteger)])
    forall a. a -> QueryT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return st -> [(SBool, VC st SInteger)]
    post
            wp st
    start (Seq (Stmt st
    s:[Stmt st]
    ss))          st -> [(SBool, VC st SInteger)]
    post = st
    -> Stmt st
    -> (st -> [(SBool, VC st SInteger)])
    -> Query (st -> [(SBool, VC st SInteger)])
    wp st
    start Stmt st
    s ((st -> [(SBool, VC st SInteger)])
     -> Query (st -> [(SBool, VC st SInteger)]))
    -> Query (st -> [(SBool, VC st SInteger)])
    -> Query (st -> [(SBool, VC st SInteger)])
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< st
    -> Stmt st
    -> (st -> [(SBool, VC st SInteger)])
    -> Query (st -> [(SBool, VC st SInteger)])
    wp st
    start ([Stmt st] -> Stmt st
    forall st. [Stmt st] -> Stmt st
    Seq [Stmt st]
    ss) st -> [(SBool, VC st SInteger)]
    post

            -- While loop, where all the WP magic happens!
            wp st
    start (While String
    nm st -> SBool
    inv Maybe (Measure st)
    mm st -> SBool
    cond Stmt st
    body) st -> [(SBool, VC st SInteger)]
    post = do
                    st
    st'  <- QueryT IO st
    forall (m :: * -> *) a. Queriable m a => QueryT m a
    create

                    let noMeasure :: Bool
    noMeasure = Maybe (Measure st) -> Bool
    forall a. Maybe a -> Bool
    isNothing Maybe (Measure st)
    mm
                        m :: Measure st
    m         = Maybe (Measure st) -> Measure st
    forall a. HasCallStack => Maybe a -> a
    fromJust Maybe (Measure st)
    mm
                        curM :: [SInteger]
    curM      = Measure st
    m st
    st'
                        zero :: [SInteger]
    zero      = (SInteger -> SInteger) -> [SInteger] -> [SInteger]
    forall a b. (a -> b) -> [a] -> [b]
    map (SInteger -> SInteger -> SInteger
    forall a b. a -> b -> a
    const SInteger
    0) [SInteger]
    curM

                        iterates :: SBool
    iterates   = st -> SBool
    inv st
    st' SBool -> SBool -> SBool
    .&&       st -> SBool
    cond st
    st'
                        terminates :: SBool
    terminates = st -> SBool
    inv st
    st' SBool -> SBool -> SBool
    .&& SBool -> SBool
    sNot (st -> SBool
    cond st
    st')

                    -- Condition 1: Invariant must hold prior to loop entry
                    st -> [(SBool, VC st SInteger)]
    invHoldsPrior <- st
    -> Stmt st
    -> (st -> [(SBool, VC st SInteger)])
    -> Query (st -> [(SBool, VC st SInteger)])
    wp st
    start Stmt st
    forall st. Stmt st
    Skip (\st
    st -> [(st -> SBool
    inv st
    st, String -> st -> VC st SInteger
    forall st m. String -> st -> VC st m
    InvariantPre String
    nm st
    st)])

                    -- Condition 2: If we iterate, invariant must be maitained by the body
                    st -> [(SBool, VC st SInteger)]
    invMaintained <- st
    -> Stmt st
    -> (st -> [(SBool, VC st SInteger)])
    -> Query (st -> [(SBool, VC st SInteger)])
    wp st
    st' Stmt st
    body (\st
    st -> [(SBool
    iterates SBool -> SBool -> SBool
    .=> st -> SBool
    inv st
    st, String -> st -> st -> VC st SInteger
    forall st m. String -> st -> st -> VC st m
    InvariantMaintain String
    nm st
    st' st
    st)])

                    -- Condition 3: If we terminate, invariant must be strong enough to establish the post condition
                    st -> [(SBool, VC st SInteger)]
    invEstablish <- st
    -> Stmt st
    -> (st -> [(SBool, VC st SInteger)])
    -> Query (st -> [(SBool, VC st SInteger)])
    wp st
    st' Stmt st
    body ([(SBool, VC st SInteger)] -> st -> [(SBool, VC st SInteger)]
    forall a b. a -> b -> a
    const [(SBool
    terminates SBool -> SBool -> SBool
    .=> SBool
    b, VC st SInteger
    v) | (SBool
    b, VC st SInteger
    v) <- st -> [(SBool, VC st SInteger)]
    post st
    st'])

                    -- Condition 4: If we iterate, measure must always be non-negative
                    st -> [(SBool, VC st SInteger)]
    measureNonNegative <- if Bool
    noMeasure
                                          then (st -> [(SBool, VC st SInteger)])
    -> Query (st -> [(SBool, VC st SInteger)])
    forall a. a -> QueryT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return  ([(SBool, VC st SInteger)] -> st -> [(SBool, VC st SInteger)]
    forall a b. a -> b -> a
    const [])
                                          else st
    -> Stmt st
    -> (st -> [(SBool, VC st SInteger)])
    -> Query (st -> [(SBool, VC st SInteger)])
    wp st
    st' Stmt st
    forall st. Stmt st
    Skip ([(SBool, VC st SInteger)] -> st -> [(SBool, VC st SInteger)]
    forall a b. a -> b -> a
    const [(SBool
    iterates SBool -> SBool -> SBool
    .=> [SInteger]
    curM [SInteger] -> [SInteger] -> SBool
    forall a. OrdSymbolic a => a -> a -> SBool
    .>= [SInteger]
    zero, String -> (st, [SInteger]) -> VC st SInteger
    forall st m. String -> (st, [m]) -> VC st m
    MeasureBound String
    nm (st
    st', [SInteger]
    curM))])

                    -- Condition 5: If we iterate, the measure must decrease
                    st -> [(SBool, VC st SInteger)]
    measureDecreases <- if Bool
    noMeasure
                                        then (st -> [(SBool, VC st SInteger)])
    -> Query (st -> [(SBool, VC st SInteger)])
    forall a. a -> QueryT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return  ([(SBool, VC st SInteger)] -> st -> [(SBool, VC st SInteger)]
    forall a b. a -> b -> a
    const [])
                                        else st
    -> Stmt st
    -> (st -> [(SBool, VC st SInteger)])
    -> Query (st -> [(SBool, VC st SInteger)])
    wp st
    st' Stmt st
    body (\st
    st -> let prevM :: [SInteger]
    prevM = Measure st
    m st
    st in [(SBool
    iterates SBool -> SBool -> SBool
    .=> [SInteger]
    prevM [SInteger] -> [SInteger] -> SBool
    forall a. OrdSymbolic a => a -> a -> SBool
    .< [SInteger]
    curM, String -> (st, [SInteger]) -> (st, [SInteger]) -> VC st SInteger
    forall st m. String -> (st, [m]) -> (st, [m]) -> VC st m
    MeasureDecrease String
    nm (st
    st', [SInteger]
    curM) (st
    st, [SInteger]
    prevM))])

                    -- Simply concatenate the VCs from all our conditions:
                    (st -> [(SBool, VC st SInteger)])
    -> Query (st -> [(SBool, VC st SInteger)])
    forall a. a -> QueryT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ((st -> [(SBool, VC st SInteger)])
     -> Query (st -> [(SBool, VC st SInteger)]))
    -> (st -> [(SBool, VC st SInteger)])
    -> Query (st -> [(SBool, VC st SInteger)])
    forall a b. (a -> b) -> a -> b
    $ \st
    st ->    st -> [(SBool, VC st SInteger)]
    invHoldsPrior      st
    st
                                    [(SBool, VC st SInteger)]
    -> [(SBool, VC st SInteger)] -> [(SBool, VC st SInteger)]
    forall a. [a] -> [a] -> [a]
    ++ st -> [(SBool, VC st SInteger)]
    invMaintained      st
    st'
                                    [(SBool, VC st SInteger)]
    -> [(SBool, VC st SInteger)] -> [(SBool, VC st SInteger)]
    forall a. [a] -> [a] -> [a]
    ++ st -> [(SBool, VC st SInteger)]
    invEstablish       st
    st'
                                    [(SBool, VC st SInteger)]
    -> [(SBool, VC st SInteger)] -> [(SBool, VC st SInteger)]
    forall a. [a] -> [a] -> [a]
    ++ st -> [(SBool, VC st SInteger)]
    measureNonNegative st
    st'
                                    [(SBool, VC st SInteger)]
    -> [(SBool, VC st SInteger)] -> [(SBool, VC st SInteger)]
    forall a. [a] -> [a] -> [a]
    ++ st -> [(SBool, VC st SInteger)]
    measureDecreases   st
    st'

    -- | Check correctness using the default solver. Equivalent to @'wpProveWith' 'defaultWPCfg'@.
    wpProve :: (Show res, Mergeable st, Queriable IO st, res ~ QueryResult st) => Program st -> IO (ProofResult res)
    wpProve :: forall res st.
    (Show res, Mergeable st, Queriable IO st, res ~ QueryResult st) =>
    Program st -> IO (ProofResult res)
    wpProve = WPConfig -> Program st -> IO (ProofResult res)
    forall st res.
    (Show res, Mergeable st, Queriable IO st, res ~ QueryResult st) =>
    WPConfig -> Program st -> IO (ProofResult res)
    wpProveWith WPConfig
    defaultWPCfg

    -- | Configuration for WP proofs.
    data WPConfig = WPConfig { WPConfig -> SMTConfig
    wpSolver  :: SMTConfig   -- ^ SMT Solver to use
                             , WPConfig -> Bool
    wpVerbose :: Bool        -- ^ Should we be chatty?
                             }

    -- | Default WP configuration: Uses the default solver, and is not verbose.
    defaultWPCfg :: WPConfig
    defaultWPCfg :: WPConfig
    defaultWPCfg = WPConfig { wpSolver :: SMTConfig
    wpSolver  = SMTConfig
    defaultSMTCfg
                            , wpVerbose :: Bool
    wpVerbose = Bool
    False
                            }

    -- * Concrete execution of a program

    -- | Tracking locations: Either a line (sequence) number, or an iteration count
    data Location = Line      Int
                  | Iteration Int

    -- | A 'Loc' is a nesting of locations. We store this in reverse order.
    type Loc = [Location]

    -- | Are we in a good state, or in a stuck state?
    data Status st = Good st               -- ^ Execution finished in the given state.
                   | Stuck (VC st Integer) -- ^ Execution got stuck, with the failing VC

    -- | Show instance for 'Status'
    instance Show st => Show (Status st) where
      show :: Status st -> String
    show (Good st
    st)  = String
    "Program terminated successfully. Final state:\n" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String -> [String] -> String
    forall a. [a] -> [[a]] -> [a]
    intercalate String
    "\n" [String
    "  " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    l | String
    l <- String -> [String]
    lines (st -> String
    forall a. Show a => a -> String
    show st
    st)]
      show (Stuck VC st Integer
    vc) = String
    "Program is stuck.\n" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ VC st Integer -> String
    forall a. Show a => a -> String
    show VC st Integer
    vc

    -- | Trace the execution of a program, starting from a sufficiently concrete state. (Sufficiently here means that
    -- all parts of the state that is used uninitialized must have concrete values, i.e., essentially the inputs.
    -- You can leave the "temporary" variables initialized by the program before use undefined or even symbolic.)
    -- The return value will have a 'Good' state to indicate the program ended successfully, if that is the case. The
    -- result will be 'Stuck' if the program aborts without completing: This can happen either by executing an 'Abort'
    -- statement, or some invariant gets violated, or if a metric fails to go down through a loop body.
    traceExecution :: forall st. Show st
                   => Program st            -- ^ Program
                   -> st                    -- ^ Starting state. It must be fully concrete.
                   -> IO (Status st)
    traceExecution :: forall st. Show st => Program st -> st -> IO (Status st)
    traceExecution Program{st -> SBool
    precondition :: forall st. Program st -> st -> SBool
    precondition :: st -> SBool
    precondition, Stmt st
    program :: forall st. Program st -> Stmt st
    program :: Stmt st
    program, st -> SBool
    postcondition :: forall st. Program st -> st -> SBool
    postcondition :: st -> SBool
    postcondition, Stable st
    stability :: forall st. Program st -> Stable st
    stability :: Stable st
    stability} st
    start = do

                    Status st
    status <- if Loc -> String -> SBool -> Bool
    forall a. SymVal a => Loc -> String -> SBV a -> a
    unwrap [] String
    "checking precondition" (st -> SBool
    precondition st
    start)
                              then Loc -> Stmt st -> Status st -> IO (Status st)
    go [Int -> Location
    Line Int
    1] Stmt st
    program (Status st -> IO (Status st)) -> IO (Status st) -> IO (Status st)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Loc -> st -> String -> IO (Status st)
    step [] st
    start String
    "*** Precondition holds, starting execution:"
                              else st -> VC st Integer -> String -> IO (Status st)
    giveUp st
    start (st -> VC st Integer
    forall st m. st -> VC st m
    BadPrecondition st
    start) String
    "*** Initial state does not satisfy the precondition:"

                    case Status st
    status of
                      s :: Status st
    s@Stuck{} -> Status st -> IO (Status st)
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Status st
    s
                      Good st
    end  -> if Loc -> String -> SBool -> Bool
    forall a. SymVal a => Loc -> String -> SBV a -> a
    unwrap [] String
    "checking postcondition" (st -> SBool
    postcondition st
    end)
                                   then Loc -> st -> String -> IO (Status st)
    step [] st
    end String
    "*** Program successfully terminated, post condition holds of the final state:"
                                   else st -> VC st Integer -> String -> IO (Status st)
    giveUp st
    end (st -> st -> VC st Integer
    forall st m. st -> st -> VC st m
    BadPostcondition st
    start st
    end) String
    "*** Failed, final state does not satisfy the postcondition:"

      where sLoc :: Loc -> String -> String
            sLoc :: Loc -> String -> String
    sLoc Loc
    l String
    m
              | Loc -> Bool
    forall a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null Loc
    l = String
    m
              | Bool
    True   = String
    "===> [" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String -> [String] -> String
    forall a. [a] -> [[a]] -> [a]
    intercalate String
    "." ((Location -> String) -> Loc -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map Location -> String
    sh (Loc -> Loc
    forall a. [a] -> [a]
    reverse Loc
    l)) String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "] " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    m
              where sh :: Location -> String
    sh (Line  Int
    i)     = Int -> String
    forall a. Show a => a -> String
    show Int
    i
                    sh (Iteration Int
    i) = String
    "{" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    forall a. Show a => a -> String
    show Int
    i String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "}"

            step :: Loc -> st -> String -> IO (Status st)
            step :: Loc -> st -> String -> IO (Status st)
    step Loc
    l st
    st String
    m = do String -> IO ()
    putStrLn (String -> IO ()) -> String -> IO ()
    forall a b. (a -> b) -> a -> b
    $ Loc -> String -> String
    sLoc Loc
    l String
    m
                             st -> IO ()
    printST st
    st
                             Status st -> IO (Status st)
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Status st -> IO (Status st)) -> Status st -> IO (Status st)
    forall a b. (a -> b) -> a -> b
    $ st -> Status st
    forall st. st -> Status st
    Good st
    st

            stop :: Loc -> VC st Integer -> String -> IO (Status st)
            stop :: Loc -> VC st Integer -> String -> IO (Status st)
    stop Loc
    l VC st Integer
    vc String
    m = do String -> IO ()
    putStrLn (String -> IO ()) -> String -> IO ()
    forall a b. (a -> b) -> a -> b
    $ Loc -> String -> String
    sLoc Loc
    l String
    m
                             Status st -> IO (Status st)
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Status st -> IO (Status st)) -> Status st -> IO (Status st)
    forall a b. (a -> b) -> a -> b
    $ VC st Integer -> Status st
    forall st. VC st Integer -> Status st
    Stuck VC st Integer
    vc

            giveUp :: st -> VC st Integer -> String -> IO (Status st)
            giveUp :: st -> VC st Integer -> String -> IO (Status st)
    giveUp st
    st VC st Integer
    vc String
    m = do Status st
    r <- Loc -> VC st Integer -> String -> IO (Status st)
    stop [] VC st Integer
    vc String
    m
                                st -> IO ()
    printST st
    st
                                Status st -> IO (Status st)
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Status st
    r

            dispST :: st -> String
            dispST :: st -> String
    dispST st
    st = String -> [String] -> String
    forall a. [a] -> [[a]] -> [a]
    intercalate String
    "\n" [String
    "  " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    l | String
    l <- String -> [String]
    lines (st -> String
    forall a. Show a => a -> String
    show st
    st)]

            printST :: st -> IO ()
            printST :: st -> IO ()
    printST = String -> IO ()
    putStrLn (String -> IO ()) -> (st -> String) -> st -> IO ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . st -> String
    dispST

            unwrap :: SymVal a => Loc -> String -> SBV a -> a
            unwrap :: forall a. SymVal a => Loc -> String -> SBV a -> a
    unwrap Loc
    l String
    m SBV a
    v = case SBV a -> Maybe a
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SBV a
    v of
                             Just a
    c  -> a
    c
                             Maybe a
    Nothing -> String -> a
    forall a. HasCallStack => String -> a
    error (String -> a) -> String -> a
    forall a b. (a -> b) -> a -> b
    $ [String] -> String
    unlines [ String
    ""
                                                        , String
    "*** Data.SBV.WeakestPreconditions.traceExecution:"
                                                        , String
    "***"
                                                        , String
    "***    Unable to extract concrete value:"
                                                        , String
    "***      "  String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Loc -> String -> String
    sLoc Loc
    l String
    m
                                                        , String
    "***"
                                                        , String
    "*** Make sure the starting state is fully concrete and"
                                                        , String
    "*** there are no uninterpreted functions in play!"
                                                        ]

            go :: Loc -> Stmt st -> Status st -> IO (Status st)
            go :: Loc -> Stmt st -> Status st -> IO (Status st)
    go Loc
    _   Stmt st
    _ s :: Status st
    s@Stuck{}  = Status st -> IO (Status st)
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Status st
    s
            go Loc
    loc Stmt st
    p (Good  st
    st) = Stmt st -> IO (Status st)
    analyze Stmt st
    p
              where analyze :: Stmt st -> IO (Status st)
    analyze Stmt st
    Skip = Loc -> st -> String -> IO (Status st)
    step Loc
    loc st
    st String
    "Skip"

                    analyze (Abort String
    nm) = Loc -> VC st Integer -> String -> IO (Status st)
    stop Loc
    loc (String -> st -> st -> VC st Integer
    forall st m. String -> st -> st -> VC st m
    AbortReachable String
    nm st
    start st
    st) (String -> IO (Status st)) -> String -> IO (Status st)
    forall a b. (a -> b) -> a -> b
    $ String
    "Abort command executed, labeled: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String -> String
    forall a. Show a => a -> String
    show String
    nm

                    analyze (Assign st -> st
    f) = case [String
    nm | st -> st -> (String, SBool)
    s <- Stable st
    stability, let (String
    nm, SBool
    b) = st -> st -> (String, SBool)
    s st
    st st
    st', Bool -> Bool
    not (Loc -> String -> SBool -> Bool
    forall a. SymVal a => Loc -> String -> SBV a -> a
    unwrap Loc
    loc (String
    "evaluation stability condition " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String -> String
    forall a. Show a => a -> String
    show String
    nm) SBool
    b)] of
                                           []  -> Loc -> st -> String -> IO (Status st)
    step Loc
    loc st
    st' String
    "Assign"
                                           [String]
    nms -> let comb :: String
    comb = String -> [String] -> String
    forall a. [a] -> [[a]] -> [a]
    intercalate String
    ", " [String]
    nms
                                                      bad :: VC st Integer
    bad  = String -> st -> st -> VC st Integer
    forall st m. String -> st -> st -> VC st m
    Unstable String
    comb st
    st st
    st'
                                                  in Loc -> VC st Integer -> String -> IO (Status st)
    stop Loc
    loc VC st Integer
    bad (String -> IO (Status st)) -> String -> IO (Status st)
    forall a b. (a -> b) -> a -> b
    $ String
    "Stability condition fails for: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String -> String
    forall a. Show a => a -> String
    show String
    comb
                        where st' :: st
    st' = st -> st
    f st
    st

                    analyze (If st -> SBool
    c Stmt st
    tb Stmt st
    eb)
                      | Bool
    branchTrue       = Loc -> Stmt st -> Status st -> IO (Status st)
    go (Int -> Location
    Line Int
    1 Location -> Loc -> Loc
    forall a. a -> [a] -> [a]
    : Loc
    loc) Stmt st
    tb (Status st -> IO (Status st)) -> IO (Status st) -> IO (Status st)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Loc -> st -> String -> IO (Status st)
    step Loc
    loc st
    st String
    "Conditional, taking the \"then\" branch"
                      | Bool
    True             = Loc -> Stmt st -> Status st -> IO (Status st)
    go (Int -> Location
    Line Int
    2 Location -> Loc -> Loc
    forall a. a -> [a] -> [a]
    : Loc
    loc) Stmt st
    eb (Status st -> IO (Status st)) -> IO (Status st) -> IO (Status st)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Loc -> st -> String -> IO (Status st)
    step Loc
    loc st
    st String
    "Conditional, taking the \"else\" branch"
                      where branchTrue :: Bool
    branchTrue = Loc -> String -> SBool -> Bool
    forall a. SymVal a => Loc -> String -> SBV a -> a
    unwrap Loc
    loc String
    "evaluating the test condition" (st -> SBool
    c st
    st)

                    analyze (Seq [Stmt st]
    stmts)  = [Stmt st] -> Int -> Status st -> IO (Status st)
    walk [Stmt st]
    stmts Int
    1 (st -> Status st
    forall st. st -> Status st
    Good st
    st)
                      where walk :: [Stmt st] -> Int -> Status st -> IO (Status st)
    walk []     Int
    _ Status st
    is = Status st -> IO (Status st)
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Status st
    is
                            walk (Stmt st
    s:[Stmt st]
    ss) Int
    c Status st
    is = [Stmt st] -> Int -> Status st -> IO (Status st)
    walk [Stmt st]
    ss (Int
    cInt -> Int -> Int
    forall a. Num a => a -> a -> a
    +Int
    1) (Status st -> IO (Status st)) -> IO (Status st) -> IO (Status st)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Loc -> Stmt st -> Status st -> IO (Status st)
    go (Int -> Location
    Line Int
    c Location -> Loc -> Loc
    forall a. a -> [a] -> [a]
    : Loc
    loc) Stmt st
    s Status st
    is

                    analyze (While String
    loopName st -> SBool
    invariant Maybe (Measure st)
    mbMeasure st -> SBool
    condition Stmt st
    body)
                       | st -> Bool
    currentInvariant st
    st
                       = Int -> st -> Maybe [Integer] -> Status st -> IO (Status st)
    while Int
    1 st
    st Maybe [Integer]
    forall a. Maybe a
    Nothing (st -> Status st
    forall st. st -> Status st
    Good st
    st)
                       | Bool
    True
                       = Loc -> VC st Integer -> String -> IO (Status st)
    stop Loc
    loc (String -> st -> VC st Integer
    forall st m. String -> st -> VC st m
    InvariantPre String
    loopName st
    st) (String -> IO (Status st)) -> String -> IO (Status st)
    forall a b. (a -> b) -> a -> b
    $ String -> String
    tag String
    "invariant fails to hold prior to loop entry"
                       where tag :: String -> String
    tag String
    s = String
    "Loop " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String -> String
    forall a. Show a => a -> String
    show String
    loopName String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ": " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    s

                             hasMeasure :: Bool
    hasMeasure = Maybe (Measure st) -> Bool
    forall a. Maybe a -> Bool
    isJust Maybe (Measure st)
    mbMeasure
                             measure :: Measure st
    measure    = Maybe (Measure st) -> Measure st
    forall a. HasCallStack => Maybe a -> a
    fromJust Maybe (Measure st)
    mbMeasure

                             currentCondition :: st -> Bool
    currentCondition = Loc -> String -> SBool -> Bool
    forall a. SymVal a => Loc -> String -> SBV a -> a
    unwrap Loc
    loc (String -> String
    tag  String
    "evaluating the while condition") (SBool -> Bool) -> (st -> SBool) -> st -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . st -> SBool
    condition
                             currentMeasure :: st -> [Integer]
    currentMeasure   = (SInteger -> Integer) -> [SInteger] -> [Integer]
    forall a b. (a -> b) -> [a] -> [b]
    map (Loc -> String -> SInteger -> Integer
    forall a. SymVal a => Loc -> String -> SBV a -> a
    unwrap Loc
    loc (String -> String
    tag  String
    "evaluating the measure"))   ([SInteger] -> [Integer]) -> Measure st -> st -> [Integer]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Measure st
    measure
                             currentInvariant :: st -> Bool
    currentInvariant = Loc -> String -> SBool -> Bool
    forall a. SymVal a => Loc -> String -> SBV a -> a
    unwrap Loc
    loc (String -> String
    tag  String
    "evaluating the invariant")       (SBool -> Bool) -> (st -> SBool) -> st -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . st -> SBool
    invariant

                             while :: Int -> st -> Maybe [Integer] -> Status st -> IO (Status st)
    while Int
    _ st
    _      Maybe [Integer]
    _      s :: Status st
    s@Stuck{}  = Status st -> IO (Status st)
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Status st
    s
                             while Int
    c st
    prevST Maybe [Integer]
    mbPrev (Good  st
    is)
                               | Bool -> Bool
    not (st -> Bool
    currentCondition st
    is)
                               = Loc -> st -> String -> IO (Status st)
    step Loc
    loc st
    is (String -> IO (Status st)) -> String -> IO (Status st)
    forall a b. (a -> b) -> a -> b
    $ String -> String
    tag String
    "condition fails, terminating"
                               | Bool -> Bool
    not (st -> Bool
    currentInvariant st
    is)
                               = Loc -> VC st Integer -> String -> IO (Status st)
    stop Loc
    loc (String -> st -> st -> VC st Integer
    forall st m. String -> st -> st -> VC st m
    InvariantMaintain String
    loopName st
    prevST st
    is) (String -> IO (Status st)) -> String -> IO (Status st)
    forall a b. (a -> b) -> a -> b
    $ String -> String
    tag String
    "invariant fails to hold in iteration " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    forall a. Show a => a -> String
    show Int
    c
                               | Bool
    hasMeasure Bool -> Bool -> Bool
    && [Integer]
    mCur [Integer] -> [Integer] -> Bool
    forall a. Ord a => a -> a -> Bool
    < [Integer]
    zero
                               = Loc -> VC st Integer -> String -> IO (Status st)
    stop Loc
    loc (String -> (st, [Integer]) -> VC st Integer
    forall st m. String -> (st, [m]) -> VC st m
    MeasureBound String
    loopName (st
    is, [Integer]
    mCur)) (String -> IO (Status st)) -> String -> IO (Status st)
    forall a b. (a -> b) -> a -> b
    $ String -> String
    tag String
    "measure must be non-negative, evaluated to: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ [Integer] -> String
    forall a. Show a => a -> String
    show [Integer]
    mCur
                               | Bool
    hasMeasure, Just [Integer]
    mPrev <- Maybe [Integer]
    mbPrev, [Integer]
    mCur [Integer] -> [Integer] -> Bool
    forall a. Ord a => a -> a -> Bool
    >= [Integer]
    mPrev
                               = Loc -> VC st Integer -> String -> IO (Status st)
    stop Loc
    loc (String -> (st, [Integer]) -> (st, [Integer]) -> VC st Integer
    forall st m. String -> (st, [m]) -> (st, [m]) -> VC st m
    MeasureDecrease String
    loopName (st
    prevST, [Integer]
    mPrev) (st
    is, [Integer]
    mCur)) (String -> IO (Status st)) -> String -> IO (Status st)
    forall a b. (a -> b) -> a -> b
    $ String -> String
    tag (String -> String) -> String -> String
    forall a b. (a -> b) -> a -> b
    $ String
    "measure failed to decrease, prev = " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ [Integer] -> String
    forall a. Show a => a -> String
    show [Integer]
    mPrev String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ", current = " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ [Integer] -> String
    forall a. Show a => a -> String
    show [Integer]
    mCur
                               | Bool
    True
                               = do Status st
    nextState <- Loc -> Stmt st -> Status st -> IO (Status st)
    go (Int -> Location
    Iteration Int
    c Location -> Loc -> Loc
    forall a. a -> [a] -> [a]
    : Loc
    loc) Stmt st
    body (Status st -> IO (Status st)) -> IO (Status st) -> IO (Status st)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Loc -> st -> String -> IO (Status st)
    step Loc
    loc st
    is (String -> String
    tag String
    "condition holds, executing the body")
                                    Int -> st -> Maybe [Integer] -> Status st -> IO (Status st)
    while (Int
    cInt -> Int -> Int
    forall a. Num a => a -> a -> a
    +Int
    1) st
    is ([Integer] -> Maybe [Integer]
    forall a. a -> Maybe a
    Just [Integer]
    mCur) Status st
    nextState
                               where mCur :: [Integer]
    mCur = st -> [Integer]
    currentMeasure st
    is
                                     zero :: [Integer]
    zero = (Integer -> Integer) -> [Integer] -> [Integer]
    forall a b. (a -> b) -> [a] -> [b]
    map (Integer -> Integer -> Integer
    forall a b. a -> b -> a
    const Integer
    0) [Integer]
    mCur

    {- HLint ignore traceExecution "Use fromMaybe" -}