content: {-# LANGUAGE MultiParamTypeClasses, FlexibleContexts #-}
  module ProofObligation (
                          ProofObligation(..),
                          HasProve(..), ProofResult(..), MsgFn(..), MsgTuple,
                          warnUnlessProof, errorUnlessProof,
                          checkProofs
                         ) where
  
  import Error(EMsg, ErrorHandle, bsWarningsAndErrors)
  import PPrint
  
  import Control.Monad(when)
  import Control.Monad.Trans(MonadIO, liftIO)
  import Data.List(sortBy, groupBy)
  
  -- import Debug.Trace
  
  -- A proof attempt to can yield one of 3 results
  data ProofResult = Proven | Disproven | Inconclusive
    deriving (Eq, Show)
  
  -- This class encapsulates the property of supporting proofs
  class HasProve a m where
    prove :: a -> m ProofResult
  
  -- This is a generic framework for recording different types
  -- of provable statements.  The instance declarations for
  -- various types of ProofObligations are defined elsewhere,
  -- to avoid recursive module dependencies.
  data ProofObligation a = ProveEq a a
                         | ProveNotEq a a
  
  instance Eq a => Eq (ProofObligation a) where
    (ProveEq x1 y1)    == (ProveEq x2 y2)    = (x1 == x2) && (y1 == y2)
    (ProveNotEq x1 y1) == (ProveNotEq x2 y2) = (x1 == x2) && (y1 == y2)
    _                  == _                  = False
  
  instance Show a => Show (ProofObligation a) where
    show (ProveEq    x y) = (show x) ++ " == " ++ (show y)
    show (ProveNotEq x y) = (show x) ++ " != " ++ (show y)
  
  instance PPrint a => PPrint (ProofObligation a) where
    pPrint d p (ProveEq    x y) = (pPrint d 0 x)<+>(text "==")<+>(pPrint d 0 y)
    pPrint d p (ProveNotEq x y) = (pPrint d 0 x)<+>(text "!=")<+>(pPrint d 0 y)
  
  -- This allows us to group related tests to produce better
  -- error messages
  data MsgFn =
    MsgFn { mf_ident :: String
          , mf_fn    :: ProofResult -> MsgTuple -> MsgTuple
          }
  
  -- (warnings, demotable errors, errors)
  type MsgTuple = ([EMsg], [EMsg], [EMsg])
  
  instance Eq MsgFn where
    mf1 == mf2 = (mf_ident mf1) == (mf_ident mf2)
  
  instance Ord MsgFn where
    compare mf1 mf2 = compare (mf_ident mf1) (mf_ident mf2)
  
  instance Show MsgFn where
    show (MsgFn s _) = s
  
  instance PPrint MsgFn where
    pPrint _ _ x = text (show x)
  
  errorUnlessProof :: [EMsg] -> ProofResult -> MsgTuple -> MsgTuple
  errorUnlessProof _  Proven (ws, ds, es) = (ws, ds, es)
  errorUnlessProof em _      (ws, ds, es) = (ws, ds, es ++ em)
  
  warnUnlessProof :: [EMsg] -> ProofResult -> MsgTuple -> MsgTuple
  warnUnlessProof _  Proven (ws, ds, es) = (ws, ds, es)
  warnUnlessProof wm _      (ws, ds, es) = (ws ++ wm, ds, es)
  
  -- Check a set of mixed proof obligations by first grouping them
  -- by message function type and then checking each group
  checkProofs :: (MonadIO m, HasProve (ProofObligation a) m) =>
                 ErrorHandle -> [(ProofObligation a, MsgFn)] -> m Bool
  checkProofs _ [] = return True
  checkProofs errh ps =
    do let cmpSnd (_,x1) (_,x2) = x1 `compare` x2
           eqSnd  (_,x1) (_,x2) = x1 == x2
           groups = groupBy eqSnd (sortBy cmpSnd ps)
       bs <- mapM (checkProofSet errh) groups
       return (and bs)
  
  -- Check one group of proof obligations
  checkProofSet :: (MonadIO m, HasProve (ProofObligation a) m) =>
                   ErrorHandle -> [(ProofObligation a, MsgFn)] -> m Bool
  checkProofSet _ [] = return True
  checkProofSet errh ps =
    do results <- mapM (prove . fst) ps
       let fns          = [ fn | (_,(MsgFn _ fn)) <- ps ]
           (warns, demerrs, errs) = buildErrs (zip fns results) ([], [], [])
       when (any (not . null) [warns, demerrs, errs]) $
           liftIO (bsWarningsAndErrors errh warns demerrs errs)
       return ((null demerrs) && (null errs))
    where buildErrs []            we = we
          buildErrs ((fn,res):xs) we = buildErrs xs (fn res we)
  