{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiWayIf #-}
{-# LANGUAGE OverloadedStrings #-}
-- | This module provides various default formatters for outputting
-- information in human readable form.  Alternative versions should be
-- used where appropriate.

module Crux.FormatOut
  (
    sayWhatResultStatus
  , sayWhatFailedGoals
  )
where

import qualified Data.BitVector.Sized as BV
import           Data.Foldable ( toList )
import           Data.Sequence (Seq)
import qualified Data.Text as Text (Text)
import           Prettyprinter ( (<+>) )
import qualified Prettyprinter as PP
import qualified Prettyprinter.Render.Text as PPR

import           What4.Expr (GroundValueWrapper(..), GroundValue)
import           What4.BaseTypes
import           What4.ProgramLoc

import           Lang.Crucible.Backend (CrucibleEvent(..))
import qualified Lang.Crucible.Simulator.SimError as CSE

import           Crux.Types

sayWhatResultStatus :: CruxSimulationResult -> SayWhat
sayWhatResultStatus (CruxSimulationResult cmpl gls) =
  let tot        = sum (totalProcessedGoals . fst <$> gls)
      proved     = sum (provedGoals . fst <$> gls)
      disproved  = sum (disprovedGoals . fst <$> gls)
      incomplete = sum (incompleteGoals . fst <$> gls)
      unknown    = tot - (proved + disproved + incomplete)
      goalSummary = if tot == 0 then
                      "All goals discharged through internal simplification."
                    else
                      PP.nest 2 $
                      PP.vcat [ "Goal status:"
                              , "Total:" <+> PP.pretty tot
                              , "Proved:" <+> PP.pretty proved
                              , "Disproved:" <+> PP.pretty disproved
                              , "Incomplete:" <+> PP.pretty incomplete
                              , "Unknown:" <+> PP.pretty unknown
                              ]
  in SayMore
     (SayWhat Simply "Crux" $ ppToText goalSummary)
     $ if | disproved > 0 ->
              SayWhat Fail "Crux" "Overall status: Invalid."
          | incomplete > 0 || cmpl == ProgramIncomplete ->
              SayWhat Warn "Crux" "Overall status: Unknown (incomplete)."
          | unknown > 0 -> SayWhat Warn "Crux" "Overall status: Unknown."
          | proved == tot -> SayWhat OK "Crux" "Overall status: Valid."
          | otherwise ->
              SayWhat Fail "Crux" "Internal error computing overall status."

sayWhatFailedGoals :: Bool -> Bool -> Seq ProvedGoals -> SayWhat
sayWhatFailedGoals skipIncompl showVars allGls =
  if null allDocs
     then SayNothing
     else SayWhat Fail "Crux" $ ppToText $ PP.vsep allDocs
 where
  failedDoc = \case
    Branch gls1 gls2 -> failedDoc gls1 <> failedDoc gls2
    ProvedGoal{} -> []
    NotProvedGoal _asmps err ex _locs mdl s ->
      if | skipIncompl, CSE.SimError _ (CSE.ResourceExhausted _) <- err -> []
         | Just (_m,evs) <- mdl ->
             [ PP.nest 2 $ PP.vcat (
               [ "Found counterexample for verification goal"
               -- n.b. prefer the prepared pretty explanation, but
               -- if not available, use the NotProved information.
               -- Don't show both: they tend to be duplications.
               , if null (show ex) then PP.viaShow err else ex
               ] -- if `showVars` is set, print the sequence of symbolic
                 -- variable events that led to this failure
                 ++ if showVars then
                      ["Symbolic variables:", PP.indent 2 (PP.vcat (ppVars evs))]
                    else []
                 -- print abducts, if any
                 ++ if s /= [] then
                      let numFacts = length s
                          -- NB: If you update the contents of this error
                          -- message, make sure to update the corresponding
                          -- regexes that check for this in
                          -- crux-llvm/test/Test.hs.
                          herald = PP.plural
                                     "The following fact"
                                     ("One of the following"
                                        PP.<+> PP.viaShow numFacts
                                        PP.<+> "facts")
                                     numFacts PP.<+> "would entail the goal" in
                      herald : (map (\x -> PP.pretty ('*' : ' ' : x)) s)
                    else [])]
         | otherwise ->
           [ PP.nest 2 $ PP.vcat [ "Failed to prove verification goal", ex ] ]

  ppVars evs =
    do CreateVariableEvent loc nm tpr (GVW v) <- evs
       pure (ppVarEvent loc nm tpr v)

  ppVarEvent loc nm tpr v =
    PP.pretty nm PP.<+> "=" PP.<+> ppVal tpr v PP.<+> "at" PP.<+> PP.pretty (plSourceLoc loc)

  ppVal :: BaseTypeRepr tp -> GroundValue tp -> PP.Doc ann
  ppVal tpr v = case tpr of
    BaseBVRepr _w -> PP.viaShow (BV.asUnsigned v)
    BaseFloatRepr _fpp -> PP.viaShow v
    BaseRealRepr -> PP.viaShow v
    _ -> "<unknown>" PP.<+> PP.viaShow tpr

  allDocs = mconcat (failedDoc <$> toList allGls)



ppToText :: PP.Doc ann -> Text.Text
ppToText = PPR.renderStrict . PP.layoutPretty PP.defaultLayoutOptions