content: {-# 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)
  