{-# LANGUAGE CPP #-}
{- |
Module      :  ./CASL/CompositionTable/ModelChecker.hs
Description :  checks validity of models regarding a composition table
Copyright   :  (c) Uni Bremen 2005
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  Christian.Maeder@dfki.de
Stability   :  provisional
Portability :  non-portable

checks validity of models regarding a composition table
-}

module CASL.CompositionTable.ModelChecker (modelCheck) where

import CASL.CompositionTable.CompositionTable
import CASL.CompositionTable.ModelTable
import CASL.CompositionTable.ModelFormula
import CASL.AS_Basic_CASL
import CASL.Fold
import CASL.Sign
import CASL.ToDoc
import CASL.Logic_CASL
import Logic.Logic

import Common.AS_Annotation
import Common.Result
import Common.Id
import qualified Common.Lib.MapSet as MapSet
import Common.Utils

import qualified Data.Set as Set
import qualified Data.IntSet as IntSet
import qualified Data.IntMap as IntMap
import qualified Data.Map as Map

import Data.Function
import Data.Maybe
import Data.List

modelCheck :: Int -> (Sign () (), [Named (FORMULA ())])
           -> Table2 -> Result ()
modelCheck c (sign, sent) t = do
  let sm = Map.fromList $ extractAnnotations (annoMap sign)
  mapM_ (modelCheckTest c sm sign t) sent

extractAnnotations :: MapSet.MapSet Symbol Annotation -> [(OP_SYMB, String)]
extractAnnotations m =
    catMaybes [extractAnnotation (a, b) | (a, b) <- MapSet.toList m]

extractAnnotation :: (Symbol, [Annotation]) -> Maybe (OP_SYMB, String)
extractAnnotation (Symbol symbname symbtype, set) = case symbtype of
    OpAsItemType _ -> Just (createOpSymb symbname symbtype, getAnno set)
    _ -> Nothing

createOpSymb :: Id -> SymbType -> OP_SYMB
createOpSymb i st = case st of
  OpAsItemType ty -> Qual_op_name i (toOP_TYPE ty) nullRange
  _ -> error "CASL.CompositionTable.ModelChecker.createOpSymb"

getAnno :: [Annotation] -> String
getAnno as = case as of
   [a] -> getAnnoAux a
   _ -> "failure"

getAnnoAux :: Annotation -> String
getAnnoAux a = case a of
    Unparsed_anno (Annote_word word) _ _ -> word
    _ -> ""

modelCheckTest :: Int -> Map.Map OP_SYMB String -> Sign () () -> Table2
  -> Named (FORMULA ()) -> Result ()
modelCheckTest c symbs sign t x = let
    (n, d) = modelCheckTest1 c (sentence x) t symbs
    fstr = shows (printTheoryFormula (mapNamed (simplify_sen CASL sign) x)) "\n"
      in if null d
      then hint () ("Formula succeeded:\n" ++ fstr) nullRange
      else warning () ("Formula failed:\n" ++ fstr ++ show n
               ++ " counter example" ++ (if n > 1 then "s" else "")
               ++ ":\n" ++ intercalate "\n" d) nullRange

ifind :: Int -> IntMap.IntMap a -> a
ifind = IntMap.findWithDefault (error "CompositionTable.ifind")

modelCheckTest1 :: Int -> FORMULA () -> Table2 -> Map.Map OP_SYMB String
  -> (Int, [String])
modelCheckTest1 c sen t symbs = let
  vs = number $ Set.toList $ vars sen
  vm = Map.fromList vs
  rm = IntMap.fromList $ map (\ (a, b) -> (b, show a)) vs
  nf = foldFormula (fromCASL symbs vm) sen
  in case nf of
    Quant quant decl f -> calculateQuantification (Just c) (`ifind` rm)
        quant f t $ generateVariableAssignments decl t
    _ -> if calculateFormula t IntMap.empty nf then
       (0, []) else (1, ["formula as given above."])

calculateQuantification :: Maybe Int -> (Int -> String) -> QUANTIFIER -> Form
  -> Table2 -> [Assignment] -> (Int, [String])
calculateQuantification mc si quant f t@(Table2 _ _ l _ _ _) vs =
      let calc ass = calculateFormula t ass f
          nD = showAssignments si l
      in case quant of
           Universal -> case mc of
             Just c -> let
               fall (c0, ds) ass = let
                 res = calc ass
                 nC0 = if res then c0 else c0 + 1
                 nDs = if res || nC0 > c then ds else nD ass : ds
                 in seq (seq nC0 nDs) (nC0, nDs)
               in foldl' fall (0, []) vs
             Nothing -> foldr (\ ass p@(_, ds) ->
               if null ds then if calc ass then p else (1, [nD ass]) else p)
               (0, []) vs
           Existential -> if any calc vs then (0, []) else
               (1, ["Existential not fulfilled"])
           Unique_existential -> let
               funi ass ds = case ds of
                 _ : _ : _ -> ds
                 _ | calc ass -> nD ass : ds
                 _ -> ds
             in case foldr funi [] vs of
             [] -> (1, ["Unique Existential not fulfilled"])
             [_] -> (0, [])
             ds -> (1, ds)

type Assignment = IntMap.IntMap Int

showAssignments :: (Int -> String) -> IntMap.IntMap Baserel -> Assignment
  -> String
showAssignments si l xs =
    '[' : intercalate ", " (map (showSingleAssignment si l) $ IntMap.toList xs)
     ++ "]"

showSingleAssignment :: (Int -> String) -> IntMap.IntMap Baserel -> (Int, Int)
  -> String
showSingleAssignment si m (v, i) = si v ++ "->" ++ case ifind i m of
  Baserel b -> b

calculateTerm :: Assignment -> Table2 -> Term -> BSet
calculateTerm ass t trm = case trm of
    Var var -> getBaseRelForVariable var ass
    Appl opSymb terms -> applyOperation opSymb terms t ass
    Cond t1 fo t2 -> on (\ a b -> if calculateFormula t ass fo then a else b)
      (calculateTerm ass t) t1 t2

applyOperation :: Op -> [Term] -> Table2 -> Assignment -> BSet
applyOperation ra ts table@(Table2 _ id_ _ baserels cmpentries convtbl) ass =
  let err = error "CompositionTable.applyOperator"
  in case ts of
    ft : rt -> let r1 = calculateTerm ass table ft
      in case rt of
         [sd] -> case ra of
               Comp -> calculateComposition cmpentries r1
               Inter -> IntSet.intersection r1
               Union -> IntSet.union r1
               _ -> err
             $ calculateTerm ass table sd
         [] -> let (conv, inv, shortc, hom) = convtbl in case ra of
             Compl -> IntSet.difference baserels
             Conv -> calculateConverse conv
             Shortcut -> calculateConverse shortc
             Inv -> calculateConverse inv
             Home -> calculateConverse hom
             _ -> err
           $ r1
         _ -> err
    [] -> case ra of
      One -> baserels
      Iden -> IntSet.singleton id_
      Zero -> IntSet.empty
      _ -> err

intSetFold :: (Int -> b -> b) -> b -> IntSet.IntSet -> b
intSetFold =
#if __GLASGOW_HASKELL__ < 704
  IntSet.fold
#else
  IntSet.foldr'
#endif

calculateComposition :: CmpTbl -> BSet -> BSet -> BSet
calculateComposition entries rels1 rels2 = intSetFold
  (\ s1 t -> case ifind s1 entries of
      m1 -> intSetFold
         (\ s2 -> case ifind s2 m1 of
            m2 -> IntSet.union m2)
         t rels2)
  IntSet.empty rels1

calculateConverse :: ConTable -> BSet -> BSet
calculateConverse t =
    IntSet.unions . map (`ifind` t)
    . IntSet.toList

getBaseRelForVariable :: Int -> Assignment -> BSet
getBaseRelForVariable var = IntSet.singleton . ifind var

calculateFormula :: Table2 -> Assignment -> Form -> Bool
calculateFormula t varass qf = case qf of
    Quant q vardecls f ->
       null . snd . calculateQuantification Nothing show q f t
         $ appendVariableAssignments varass vardecls t
    Junct j formulas -> (if j then all else any)
        (calculateFormula t varass) formulas
    Impl isImpl f1 f2 -> on (if isImpl then (<=) else (==))
                 (calculateFormula t varass) f1 f2
    Neg f -> not $ calculateFormula t varass f
    Const b -> b
    Eq term1 term2 -> on (==) (calculateTerm varass t) term1 term2

generateVariableAssignments :: [Int] -> Table2 -> [Assignment]
generateVariableAssignments vs =
  gVAs vs . IntSet.toList . getBaseRelations

gVAs :: [Int] -> [Int] -> [Assignment]
gVAs vs brs = foldr (\ v rs -> [IntMap.insert v b r | b <- brs, r <- rs])
  [IntMap.empty] vs

getBaseRelations :: Table2 -> BSet
getBaseRelations (Table2 _ _ _ br _ _) = br

appendVariableAssignments :: Assignment -> [Int] -> Table2 -> [Assignment]
appendVariableAssignments vm decls t =
     map (`IntMap.union` vm) (generateVariableAssignments decls t)
