content: {-# LANGUAGE FlexibleContexts, FlexibleInstances, TypeSynonymInstances #-}
  {- |
  Module      :  ./CSL/Verification.hs
  Description :  Generation of Verification Conditions
  Copyright   :  (c) Ewaryst Schulz, DFKI Bremen 2011
  License     :  GPLv2 or higher, see LICENSE.txt
  
  Maintainer  :  ewaryst.schulz@dfki.de
  Stability   :  experimental
  Portability :  non-portable (via imports)
  
  This module provides functionality for the generation of verification conditions
  during program evaluation. The output is in Isabelle Syntax.
  -}
  
  module CSL.Verification where
  
  -- import qualified Data.Map as Map
  import qualified Data.Set as Set
  import CSL.Interpreter
  import CSL.Transformation
  import CSL.DependencyGraph
  import CSL.AS_BASIC_CSL
  import CSL.ASUtils
  import CSL.Print_AS
  
  import Common.Doc
  import Common.DocUtils
  
  import System.IO
  import Control.Monad.Reader
  import Control.Monad.Error (MonadError (..))
  
  {- import Control.Monad.Trans (MonadIO (..))
  import Control.Monad (when) -}
  
  {- ----------------------------------------------------------------------
  Verification Conditions
  ---------------------------------------------------------------------- -}
  
  {- Given an instantiated constant this data structure keeps
  
  * the value of this constant looked up in the assignment store
  
  * for function constants its definition (looked up in the assignment store)
  
  * the for this constant generated verification condition
  
  data VCData = VCData
      { vcValue :: EXPRESSION
      , vcDef :: Maybe AssDefinition
      , vcCondition :: EXPRESSION
      }
  
  type VCMap = Map.Map InstantiatedConstant VCData
  
  -}
  
  
  -- | Extra functionality of 'AssignmentStore's for VC generation
  class AssignmentStore m => VCGenerator m where
      addVC :: EvalAtom -> EXPRESSION -> m ()
  
  getVCPremises :: (Ord a) => AssignmentDepGraph a -- ^ 'DepGraph' for lookup
                -> EXPRESSION -- ^ generate premise for this term
                -> [EXPRESSION]
  getVCPremises adg e =
      let scl = Set.map SimpleConstant $ setOfUserDefined e
          f (sc, depGrAnno) = mkVCPrem sc $ annoDef depGrAnno
      in map f $ Set.toList $ upperUntilRefl (const $ const False) adg scl
  
  mkCondition :: AssDefinition -> EXPRESSION -> EXPRESSION -> EXPRESSION
  mkCondition def lhs rhs = f args where
      args = getArguments def
      f (x : l) = g x $ f l
      f _ = toExp $ if isInterval rhs then ("in", lhs, rhs)
            else ("=", lhs, rhs)
      g v b = toExp ("all", mkVar v, b)
  
  mkVCPrem :: ConstantName -> AssDefinition -> EXPRESSION
  mkVCPrem n def = mkCondition def (toExp ( "::"
                                         , toExp (n, map mkVar $ getArguments def)
                                         , OP_real)) $ getDefiniens def
  
  mkVC :: ConstantName
       -> AssDefinition
       -> EXPRESSION -- ^ the evaluated term for the constant
       -> [EXPRESSION] -- ^ a list of premises from assignment graph
       -> EXPRESSION
  mkVC _ def evalE prl =
      let prem = foldl f (head prl) $ tail prl
          f a b = toExp ("and", a, b)
          conc = mkCondition def (getDefiniens def) evalE
      in if null prl then conc else toExp ("impl", prem, conc)
  
  mkBoolVC :: EXPRESSION -- ^ the Boolean term
           -> Bool -- ^ the evaluated Boolean term
           -> [EXPRESSION] -- ^ a list of premises from assignment graph
           -> EXPRESSION
  mkBoolVC e evalB prl =
      let prem = foldl f (head prl) $ tail prl
          f a b = toExp ("and", a, b)
          conc = if evalB then e else toExp ("not", e)
      in if null prl then conc else toExp ("impl", prem, conc)
  
  verifyingStepper ::
      (StepDebugger m, VCGenerator m, MonadIO m, MonadError ASError m) =>
      m () -> EvalAtom -> m Bool
  verifyingStepper prog x = do
    {- liftIO $ putStrLn $ "At step " ++ show (prettyEvalAtom x)
    liftIO $ putStrLn "" -}
    b <- evaluateAndVerify prog x
    dm <- getDebugMode
    when dm $ do
      let breakPred s = s == "q" || s == "c" || null s
      s <- readEvalPrintLoop stdin stdout "next>" breakPred
      when (s == "q") $ throwError $ ASError UserError "Quit Debugger"
      when (s == "c") $ setDebugMode False
    return b
  
  evaluateAndVerify :: (VCGenerator m) => m () -> EvalAtom -> m Bool
  evaluateAndVerify _ ea@(AssAtom n def) = do
    adg <- getDepGraph
    let prl = getVCPremises adg $ getDefiniens def
    e <- assign n def
    addVC ea $ mkVC n def e prl
    -- update the depgraph in the assignment store
    updateConstant n $ updateDefinition e def
    return True
  
  evaluateAndVerify _ ea@(CaseAtom e) = do
    adg <- getDepGraph
    let prl = getVCPremises adg e
    b <- check e
    addVC ea $ mkBoolVC e b prl
    return b
  
  evaluateAndVerify prog ea@(RepeatAtom _ _ e') = do
    prog
    adg <- getDepGraph
    let prl = getVCPremises adg e'
    b <- check e'
    addVC ea $ mkBoolVC e' b prl
    return b
  
  
  {- ----------------------------------------------------------------------
  Printing Verification Conditions
  ---------------------------------------------------------------------- -}
  
  showOpnameForVC :: OPNAME -> String
  showOpnameForVC x =
          case x of
            OP_ex -> "enclEX"
            OP_all -> "enclAll"
            OP_max -> "maxx"
            OP_min -> "minn"
            OP_or -> "|"
            OP_impl -> "-->"
            OP_and -> "&"
            _ -> showOPNAME x
  
  
  data VCPrinter = VCPrinter
  
  -- | The VCPrinter can be interpreted as an 'ExpressionPrinter'
  instance ExpressionPrinter (Reader VCPrinter) where
      getOINM = return operatorInfoNameMap
      printOpname = return . text . showOpnameForVC
      printInterval l r = return $
                          text "Interval"
                                <> parens (sepByCommas $ map (text . show) [l, r])
      printRational r = return $ text $ show nn ++ "/" ++ show dn
          where (nn, dn) = toFraction r
  
  printExpForVC :: EXPRESSION -> Doc
  printExpForVC e = doubleQuotes $ runReader (printExpression e) VCPrinter
  
  printVCForIsabelle :: EvalAtom -> String -> EXPRESSION -> Doc
  printVCForIsabelle ea s e =
      let cm = text "Verification condition for" <+> pretty ea <> text ":"
      in sep [ parens $ hcat [text "*", cm, text "*"], text "lemma"
             , doubleQuotes $ text s, text ":", printExpForVC e ]
  