{-# LANGUAGE FlexibleInstances #-}
{- |
Module      :  $Header$
Description :  QuickCheck model checker for CASL.CFOL
Copyright   :  (c) Till Mossakowski, Uni Bremen 2007
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  till@informatik.uni-bremen.de
Stability   :  provisional
Portability :  non-portable (via GUI imports, FlexibleInstances)

QuickCheck model checker for CASL.CFOL.
Initially, only finite enumeration domains are supported
-}

module CASL.QuickCheck (quickCheckProver) where

import qualified Common.AS_Annotation as AS_Anno
import qualified Common.Result as Result

import CASL.AS_Basic_CASL
import CASL.Sublogic as SL
import CASL.Sign
import CASL.Morphism
import CASL.Quantification
import CASL.ToDoc
import CASL.SimplifySen

import Logic.Prover

import Common.DocUtils
import Common.Id
import Common.ProofTree
import Common.Result
import Common.Utils (timeoutSecs)

import qualified Data.Map as Map
import Data.Maybe
import Data.List

import Control.Monad
import Control.Concurrent

import GUI.GenericATP

import Interfaces.GenericATPState

import Proofs.BatchProcessing

-- a qmodel is a certain term model used by QuickCheck
data QModel = QModel
        { sign :: CASLSign
        -- sentences determining the set of terms for a sort
        , carrierSens :: Map.Map SORT [CASLFORMULA]
        -- definitions of predicates and operations
        , predDefs :: Map.Map PRED_SYMB [([CASLTERM], CASLFORMULA)]
        , opDefs :: Map.Map OP_SYMB [([CASLTERM], CASLTERM)]
        -- currently evaluated items, for avoiding infinite recursion
        , evaluatedPreds :: [(PRED_SYMB, [CASLTERM])]
        , evaluatedOps :: [(OP_SYMB, [CASLTERM])]
        } deriving Show

{- |
  Run the QuickCheck service.
-}
runQuickCheck :: QModel
           {- ^ logical part containing the input Sign and axioms and possibly
           goals that have been proved earlier as additional axioms -}
           -> GenericConfig ProofTree -- ^ configuration to use
           -> Bool -- ^ True means save theory file
           -> String -- ^ name of the theory in the DevGraph
           -> AS_Anno.Named CASLFORMULA -- ^ goal to prove
           -> IO (ATPRetval, GenericConfig ProofTree)
           -- ^ (retval, configuration with proof status and complete output)
runQuickCheck qm cfg _saveFile _thName nGoal = do
  (stat, Result d res) <- case timeLimit cfg of
    Nothing -> return (ATPSuccess, quickCheck qm nGoal)
    Just t -> do
      mRes <- timeoutSecs t $ return $ quickCheck qm nGoal
      return $ maybe (ATPTLimitExceeded, fail "time limit exceeded")
                     (\ x -> (ATPSuccess, x)) mRes
  let fstr = show (printTheoryFormula $ AS_Anno.mapNamed
                       (simplifyCASLSen $ sign qm) nGoal)
      showDiagStrings = intercalate "\n" . map diagString -- no final newline
      diagstr = case (res, d) of
        (Just True, _) -> showDiagStrings (take 10 d)
        (_, []) -> ""
        _ -> unlines ["Formula failed: ", fstr, " some Counterexamples: "]
             ++ showDiagStrings (take 10 d)
      gstat = case res of
        Just True -> Proved True
        Just False -> Disproved
        Nothing -> openGoalStatus
      setStatus pstat = pstat { goalStatus = gstat
                              , usedProver = "QuickCheck"
                              , proofTree = ProofTree diagstr }
      cfg' = cfg { proofStatus = setStatus (proofStatus cfg)
                 , resultOutput = [diagstr] }
  return (stat, cfg')
  -- return ATPError if time is up???

-- * QModels

-- | initial QModel
makeQm :: CASLSign -> QModel
makeQm sig = QModel { sign = sig
                    , carrierSens = Map.empty
                    , predDefs = Map.empty
                    , opDefs = Map.empty
                    , evaluatedPreds = []
                    , evaluatedOps = []
                    }

insertSens :: QModel -> [AS_Anno.Named CASLFORMULA] -> QModel
insertSens = foldl insertSen

-- | insert sentences into a QModel
insertSen :: QModel -> AS_Anno.Named CASLFORMULA -> QModel
insertSen qm sen = if not $ AS_Anno.isAxiom sen then qm else
  let f = AS_Anno.sentence sen
      qm1 = case f of
               -- sort generation constraint?
               Sort_gen_ax cs _ ->
                 let s = map (\ c -> (newSort c, [f])) cs
                     ins = foldr $ uncurry $ Map.insertWith (++)
                  in qm { carrierSens = ins (carrierSens qm) s }
               -- axiom forcing empty carrier?
               Quantification Universal [Var_decl [_] s _] (Atom False _) _ ->
                 qm { carrierSens = Map.insertWith (++) s [f] (carrierSens qm) }
               _ -> qm
      insertPred p args body q =
        q { predDefs = Map.insertWith (++) p [(args, body)] (predDefs q)}
      insertOp op args body q =
        q { opDefs = Map.insertWith (++) op [(args, body)] (opDefs q) }
  in case stripAllQuant f of
  -- insert a predicate or operation definition into a QModel
   Predication predsymb args _ ->
     insertPred predsymb args trueForm qm1
   Negation (Predication predsymb args _) _ ->
     insertPred predsymb args falseForm qm1
   Relation (Predication predsymb args _) Equivalence body _ ->
     insertPred predsymb args body qm1
   Equation (Application opsymb args _) _ body _ ->
     insertOp opsymb args body qm1
   {- treat equality as special predicate symbol, for detecting inequalities
   also exploit that inequality is symmetric -}
   Negation (Equation t1 _ t2 _) _ ->
     insertPred eqSymb [t1, t2] falseForm $
       insertPred eqSymb [t2, t1] falseForm qm1
   _ -> qm1

-- | predicate symbol for equality (with dummy type)
eqSymb :: PRED_SYMB
eqSymb = mkQualPred eqId (Pred_type [] nullRange)

-- * Variable assignments

data VariableAssignment = VariableAssignment QModel [(VAR, CASLTERM)]

instance Show VariableAssignment where
  show (VariableAssignment qm assignList) = showAssignments qm assignList

showAssignments :: QModel -> [(VAR, CASLTERM)] -> String
showAssignments qm xs =
  '[' : intercalate ", " (map (showSingleAssignment qm) xs) ++ "]"

showSingleAssignment :: QModel -> (VAR, CASLTERM) -> String
showSingleAssignment qm (v, t) =
  show v ++ "->" ++ showDoc (rmTypesT (const return) (const id) (sign qm) t) ""

emptyAssignment :: QModel -> VariableAssignment
emptyAssignment qm = VariableAssignment qm []

insertAssignment :: VariableAssignment -> (VAR, CASLTERM) -> VariableAssignment
insertAssignment (VariableAssignment qm ass) (v, t) =
  VariableAssignment qm ((v, t) : ass)

concatAssignment :: VariableAssignment -> VariableAssignment
                 -> VariableAssignment
concatAssignment (VariableAssignment qm l1) (VariableAssignment _ l2) =
  VariableAssignment qm $ l1 ++ l2

-- * The quickcheck model checker

quickCheck :: QModel -> AS_Anno.Named CASLFORMULA -> Result Bool
quickCheck qm =
  calculateFormula True qm (emptyAssignment qm) . AS_Anno.sentence

calculateTerm :: QModel -> VariableAssignment -> CASLTERM -> Result CASLTERM
calculateTerm qm ass trm = case trm of
    Qual_var var _ _ -> lookupVar var ass
    Application opSymb terms _ ->
              applyOperation qm ass opSymb terms
    Sorted_term term _ _ -> calculateTerm qm ass term
    Conditional t1 fo t2 _ -> do
              res <- calculateFormula False qm ass fo
              calculateTerm qm ass $ if res then t1 else t2
    _ -> fail $ "QuickCheck.calculateTerm: unsupported: " ++ showDoc trm ""

lookupVar :: VAR -> VariableAssignment -> Result CASLTERM
lookupVar v (VariableAssignment _ ass) = case lookup v ass of
  Nothing -> fail ("no value for variable " ++ show v ++ " found")
  Just val -> return val

applyOperation :: QModel -> VariableAssignment -> OP_SYMB -> [CASLTERM]
               -> Result CASLTERM
applyOperation qm ass opsymb terms = do
  -- block infinite recursion
  when ((opsymb, terms) `elem` evaluatedOps qm)
       (fail ("infinite recursion when calculating"
              ++ show (mkAppl opsymb terms)))
  let qm' = qm { evaluatedOps = (opsymb, terms) : evaluatedOps qm }
  -- evaluate argument terms
  args <- mapM (calculateTerm qm' ass) terms
  -- find appropriate operation definition
  case Map.lookup opsymb (opDefs qm) of
    Nothing ->
      -- no operation definition? Then return unevaluated term
      return (mkAppl opsymb terms)
    Just bodies -> do
      -- bind formal to actual arguments
      (body, m) <- match bodies args $
                   showDoc (mkAppl opsymb args) ""
      let ass' = foldl insertAssignment ass m
      -- evaluate body of operation definition
      calculateTerm qm' ass' body

{- | match a list of arguments (second parameter) against a
a a list of bodies (first argument), each coming with a
list of formal parameters and a body term or formula -}
match :: [([CASLTERM], a)] -> [CASLTERM] -> String
      -> Result (a, [(VAR, CASLTERM)])
match bodies args msg =
  case mapMaybe (match1 args) bodies of
    [] -> fail ("no matching found for " ++ msg)
    subst : _ -> return subst

-- match against a single body
match1 :: [CASLTERM] -> ([CASLTERM], a) -> Maybe (a, [(VAR, CASLTERM)])
match1 args (vars, body) = do
  subst <- fmap concat $ zipWithM match2 vars args
  if consistent subst then return (body, subst) else Nothing

match2 :: CASLTERM -> CASLTERM -> Maybe [(VAR, CASLTERM)]
match2 (Qual_var v _ _) t = Just [(v, t)]
match2 (Application opsymb1 terms1 _) (Application opsymb2 terms2 _) =
   -- direct match of operation symbols?
   if opsymb1 == opsymb2 then
     fmap concat $ zipWithM match2 terms1 terms2
   -- if not, try to exploit overloading relation
    else do
      let (opsymb1', terms1', w1) = stripInj opsymb1 terms1
          (opsymb2', terms2', w2) = stripInj opsymb2 terms2
      when (opSymbName opsymb1' /= opSymbName opsymb2' || w1 /= w2) Nothing
      fmap concat $ zipWithM match2 terms1' terms2'
match2 (Sorted_term t1 _ _) t2 = match2 t1 t2
match2 t1 (Sorted_term t2 _ _) = match2 t1 t2
match2 _ _ = Nothing

-- | strip off the injections of an application
stripInj :: OP_SYMB -> [CASLTERM] -> (OP_SYMB, [CASLTERM], [SORT])
stripInj opsymb terms =
  let (opsymb', terms') =
        case (isInjName $ opSymbName opsymb, terms) of
          (True, [Application o ts _]) -> (o, ts)
          _ -> (opsymb, terms)
      strip1 t1@(Application o [t2] _) =
        if isInjName $ opSymbName o then t2 else t1
      strip1 t1 = t1
      terms'' = map strip1 terms'
  in (opsymb', terms'', map sortOfTerm terms'')

-- | is a substitution consistent with itself?
consistent :: [(VAR, CASLTERM)] -> Bool
consistent ass =
  isJust $ foldM insertAss Map.empty ass
  where
  insertAss m (v, t) =
    case Map.lookup v m of
      Just t1 -> if t == t1 then return m else Nothing
      Nothing -> Just $ Map.insert v t m

ternaryAnd :: (Result Bool, a) -> (Result Bool, a) -> (Result Bool, a)
ternaryAnd b1@(Result _ (Just False), _) _ = b1
ternaryAnd (Result d1 (Just True), _) (b2, x2) =
  (Result d1 (Just ()) >> b2, x2)
ternaryAnd (Result d1 Nothing, _) (b2@(Result _ (Just False)), x2) =
  (Result d1 (Just ()) >> b2, x2)
ternaryAnd (Result d1 Nothing, _) (b2, x2) =
  (Result d1 (Just ()) >> b2 >> Result [] Nothing, x2)

ternaryOr :: Result Bool -> Result Bool -> Result Bool
ternaryOr b1@(Result _ (Just True)) _ = b1
ternaryOr (Result d1 (Just False)) b2 = Result d1 (Just ()) >> b2
ternaryOr (Result d1 Nothing) b2@(Result _ (Just True)) =
  Result d1 (Just ()) >> b2
ternaryOr (Result d1 Nothing) b2 =
  Result d1 (Just ()) >> b2 >> Result [] Nothing

calculateFormula :: Bool -> QModel -> VariableAssignment -> CASLFORMULA
    -> Result Bool
calculateFormula isOuter qm varass f = case f of
    Quantification {} ->
       calculateQuantification isOuter qm varass f
    Junction j formulas _ ->
       let newFs = map (calculateFormula False qm varass) formulas
       in if j == Dis then foldl ternaryOr (return False) newFs else do
       let (res, f1) =
             foldl ternaryAnd (return True, f)
               (zip (map (calculateFormula False qm varass) formulas) formulas)
       when isOuter $ case maybeResult res of
         Just False ->
             justWarn () $ "Conjunction not fulfilled\n"
                         ++ "Formula that failed: " ++ showDoc f1 ""
         _ -> return ()
       res
    Relation f1 c f2 _ ->
        let res1 = calculateFormula False qm varass f1
            res2 = calculateFormula False qm varass f2
        in if c == Equivalence then liftM2 (==) res1 res2 else
               ternaryOr (fmap not res1) res2
    Negation f1 _ ->
        fmap not $ calculateFormula False qm varass f1
    Atom b _ -> return b
    Equation term1 _ term2 _ -> do
        t1 <- calculateTerm qm varass term1
        t2 <- calculateTerm qm varass term2
        equalElements qm t1 t2
    Predication predsymb terms _ ->
        applyPredicate qm varass predsymb terms
    _ -> fail $ "formula evaluation not implemented for: " ++ showDoc f ""

calculateQuantification :: Bool -> QModel -> VariableAssignment -> CASLFORMULA
                        -> Result Bool
calculateQuantification isOuter qm varass qf = case qf of
  Quantification quant vardecls f _ -> do
    assments <- generateVariableAssignments qm vardecls
    let assments' = map (`concatAssignment` varass) assments
    case quant of
      Universal -> do
        let resList = map (flip (calculateFormula False qm) f) assments'
            (res, fass) = foldl ternaryAnd (return True, emptyAssignment qm)
                                          (zip resList assments')
        when isOuter $ case maybeResult res of
          Just False ->
              justWarn () ("Universal quantification not fulfilled\n"
                          ++ "Counterexample: " ++ show fass)
          _ -> return ()
        res
      Existential ->
        foldl ternaryOr (return False)
                        (map (flip (calculateFormula False qm) f) assments')
      Unique_existential ->
        {- scan the assingments, stop scanning once the result is clear,
        using the Left constructor of the Either monad -}
        let combineEx1 state ass2 = case state of
              Right (msgsSoFar, ass1) ->
                let Result msgs res = calculateFormula False qm ass2 f
                in case (res, ass1) of
                -- the first fulfilment
                (Just True, Nothing) -> Right (msgsSoFar ++ msgs, Just ass2)
                -- the second fulfilment
                (Just True, Just ass1') ->
                    Left (msgsSoFar ++ msgs, Just (ass1', ass2))
                -- not fulfilled? Then nothing changes
                (Just False, _) -> Right (msgsSoFar ++ msgs, ass1)
                -- don't know? Then we don't know either
                (Nothing, _) -> Left (msgsSoFar ++ msgs, Nothing)
              Left _ -> state
        in case foldl combineEx1 (Right ([], Nothing)) assments' of
          Right (msgs, Just _) -> Result msgs (Just True)
          Right (msgs, Nothing) -> do
            Result msgs (Just ())
            when isOuter
              (justWarn () ("Unique Existential quantification"
                           ++ " not fulfilled: no assignment found"))
            return False
          Left (msgs, Just (ass1, ass2)) -> do
            Result msgs (Just ())
            when isOuter
              (justWarn () ("Unique Existential quantification"
                ++ " not fulfilled: at least two assignments found:\n"
                ++ show ass1 ++ "\n" ++ show ass2 ++ "\n"))
            return False
          Left (msgs, Nothing) ->
            Result msgs Nothing
  _ -> fail "calculateQuantification wrongly applied"

applyPredicate :: QModel -> VariableAssignment -> PRED_SYMB -> [CASLTERM]
               -> Result Bool
applyPredicate qm ass predsymb terms = do
  -- block infinite recursion
  when (elem (predsymb, terms) $ evaluatedPreds qm)
       (fail ("infinite recursion when calculating"
              ++ show (mkPredication predsymb terms)))
  let qm' = qm { evaluatedPreds = (predsymb, terms) : evaluatedPreds qm }
  -- evaluate argument terms
  args <- mapM (calculateTerm qm' ass) terms
  -- find appropriate predicate definition
  case Map.lookup predsymb (predDefs qm) of
    Nothing -> fail ("no predicate definition for " ++ showDoc predsymb "")
    Just bodies -> do
      -- bind formal to actual arguments
      (body, m) <- match bodies args $
                   showDoc (mkPredication predsymb args) ""
      let ass' = foldl insertAssignment ass m
      -- evaluate body of predicate definition
      calculateFormula False qm' ass' body

equalElements :: QModel -> CASLTERM -> CASLTERM -> Result Bool
equalElements qm t1 t2 =
  if t1 == t2 then return True
   else applyPredicate qm (emptyAssignment qm) eqSymb [t1, t2]

generateVariableAssignments :: QModel -> [VAR_DECL]
                            -> Result [VariableAssignment]
generateVariableAssignments qm vardecls = do
   let vars = flatVAR_DECLs vardecls
   carriers <- mapM (getCarrier qm . snd) vars
   let varsCarriers = zip (map fst vars) carriers
   return $ map (VariableAssignment qm) (gVAs varsCarriers)

gVAs :: [(VAR, [CASLTERM])] -> [[(VAR, CASLTERM)]]
gVAs [] = [[]]
gVAs ((v, carrier) : vs) = let
    rs = gVAs vs
    fs = map (\ b -> (v, b)) carrier
    in [f : r | f <- fs, r <- rs]


-- | check whether some formula leads to term generation of a sort
termSort :: CASLFORMULA -> Maybe (SORT, [CASLTERM])
-- sort generation constraint
termSort (Sort_gen_ax constr _) =
  case sorts of
     -- at the moment, we only treat one-sort constraints with constants
     [s] -> if all constant ops
             then Just (s, map mkTerm ops)
             else Nothing
     _ -> Nothing
    where (sorts, ops, _) = recover_Sort_gen_ax constr
          constant (Qual_op_name _ (Op_type _ [] _ _) _) = True
          constant _ = False
          mkTerm op = mkAppl op []
-- axiom forcing empty carrier
termSort (Quantification Universal [Var_decl [_] s _] (Atom False _) _) =
  Just (s, [])
termSort _ = Nothing

-- | get the carrier set for a specific sort
getCarrier :: QModel -> SORT -> Result [CASLTERM]
getCarrier qm s =
  case Map.lookup s (carrierSens qm) of
    Nothing -> fail ("sort " ++ show s ++ " is not generated")
    Just sens -> case mapMaybe termSort sens of
      [] -> fail ("sort " ++ show s ++ " is not generated by constants")
      (_, terms) : _ -> return terms
  -- todo: generalise this

-- * Interfacing to Hets prover interface

{- | The Prover implementation. First runs the batch prover (with
  graphical feedback), then starts the GUI prover. -}
quickCheckProver :: Prover CASLSign CASLFORMULA CASLMor CASL_Sublogics ProofTree
quickCheckProver = (mkProverTemplate "QuickCheck"
  (SL.top { has_part = False, which_logic = SL.FOL }) quickCheckGUI)
  { proveCMDLautomaticBatch = Just quickCheckCMDLautomaticBatch }

{- |
  Record for prover specific functions. This is used by both GUI and command
  line interface.
-}

atpFun :: String -- ^ theory name
       -> ATPFunctions CASLSign CASLFORMULA CASLMor ProofTree QModel
atpFun _thName = ATPFunctions
    { initialProverState = \ sig sens _ -> insertSens (makeQm sig) sens,
      atpTransSenName = id,
      atpInsertSentence = insertSen,
      goalOutput = \ _ _ _ -> do
            putStrLn "No display of output yet"
            return "",
      proverHelpText =
        "QuickCheck tries to evaluate sentences in term generated models. " ++
        "This only works if your theory contains enough generated or " ++
        "freely generated datatypes.",
      batchTimeEnv = "HETS_SPASS_BATCH_TIME_LIMIT",
      fileExtensions = FileExtensions {problemOutput = ".none1",
                                      proverOutput = ".none2",
                                      theoryConfiguration = ".none3"},
      runProver = runQuickCheck,
      createProverOptions = const [] }

-- ** GUI

{- |
  Invokes the generic prover GUI. SPASS specific functions are omitted by
  data type ATPFunctions.
-}
quickCheckGUI :: String -- ^ theory name
           -> Theory CASLSign CASLFORMULA ProofTree
           {- ^ theory consisting of a signature
           and a list of named sentences -}
           -> [FreeDefMorphism CASLFORMULA CASLMor] -- ^ freeness constraints
           -> IO [ProofStatus ProofTree] -- ^ proof status for each goal
quickCheckGUI thName th freedefs = genericATPgui (atpFun thName) True
    (proverName quickCheckProver) thName th freedefs emptyProofTree

-- ** command line function

{- |
  Implementation of 'Logic.Prover.proveCMDLautomaticBatch' which provides an
  automatic command line interface to the QuickCheck prover via MathServe.
  QuickCheck specific functions are omitted by data type ATPFunctions.
-}
quickCheckCMDLautomaticBatch ::
           Bool -- ^ True means include proved theorems
        -> Bool -- ^ True means save problem file
        -> MVar (Result.Result [ProofStatus ProofTree])
           -- ^ used to store the result of the batch run
        -> String -- ^ theory name
        -> TacticScript -- ^ default tactic script
        -> Theory CASLSign CASLFORMULA ProofTree {- ^ theory consisting of a
           signature and a list of named sentences -}
        -> [FreeDefMorphism CASLFORMULA CASLMor] -- ^ freeness constraints
        -> IO (ThreadId, MVar ())
           {- ^ fst: identifier of the batch thread for killing it
           snd: MVar to wait for the end of the thread -}
quickCheckCMDLautomaticBatch inclProvedThs saveProblem_batch resultMVar
                        thName defTS th freedefs =
    genericCMDLautomaticBatch (atpFun thName) inclProvedThs saveProblem_batch
        resultMVar (proverName quickCheckProver) thName
        (parseTacticScript batchTimeLimit [] defTS) th freedefs emptyProofTree
