{- |
Module      :  $Header$
Copyright   :  (c) Christian Maeder, Uni Bremen 2004-2005
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  luecke@informatik.uni-bremen.de
Stability   :  provisional
Portability :  portable

static analysis of modal logic parts
-}

module Modal.StatAna (basicModalAnalysis, minExpForm) where

import Modal.AS_Modal
import Modal.Print_AS ()
import Modal.ModalSign

import CASL.Sign
import CASL.MixfixParser
import CASL.StaticAna
import CASL.AS_Basic_CASL
import CASL.ShowMixfix
import CASL.Overload
import CASL.Quantification

import Common.AS_Annotation
import Common.GlobalAnnotations
import Common.Keywords
import Common.Lib.State
import Common.Id
import Common.Result
import Common.ExtSign
import qualified Common.Lib.MapSet as MapSet

import qualified Data.Map as Map
import qualified Data.Set as Set
import Data.List as List
import Data.Function

instance TermExtension M_FORMULA where
    freeVarsOfExt sign (BoxOrDiamond _ _ f _) = freeVars sign f

basicModalAnalysis
  :: (BASIC_SPEC M_BASIC_ITEM M_SIG_ITEM M_FORMULA,
      Sign M_FORMULA ModalSign, GlobalAnnos)
  -> Result (BASIC_SPEC M_BASIC_ITEM M_SIG_ITEM M_FORMULA,
             ExtSign (Sign M_FORMULA ModalSign) Symbol,
             [Named (FORMULA M_FORMULA)])
basicModalAnalysis =
    basicAnalysis minExpForm ana_M_BASIC_ITEM ana_M_SIG_ITEM ana_Mix

ana_Mix :: Mix M_BASIC_ITEM M_SIG_ITEM M_FORMULA ModalSign
ana_Mix = emptyMix
    { getSigIds = ids_M_SIG_ITEM
    , putParen = mapM_FORMULA
    , mixResolve = resolveM_FORMULA
    }

-- rigid ops will also be part of the CASL signature
ids_M_SIG_ITEM :: M_SIG_ITEM -> IdSets
ids_M_SIG_ITEM si = let e = Set.empty in case si of
    Rigid_op_items _ al _ ->
        (unite2 $ map (ids_OP_ITEM . item) al, e)
    Rigid_pred_items _ al _ ->
        ((e, e), Set.unions $ map (ids_PRED_ITEM . item) al)

mapMODALITY :: MODALITY -> MODALITY
mapMODALITY m = case m of
    Term_mod t -> Term_mod $ mapTerm mapM_FORMULA t
    _ -> m

mapM_FORMULA :: M_FORMULA -> M_FORMULA
mapM_FORMULA (BoxOrDiamond b m f ps) =
    BoxOrDiamond b (mapMODALITY m) (mapFormula mapM_FORMULA f) ps

resolveMODALITY :: MixResolve MODALITY
resolveMODALITY ga ids m = case m of
    Term_mod t -> fmap Term_mod $ resolveMixTrm mapM_FORMULA
                  resolveM_FORMULA ga ids t
    _ -> return m

resolveM_FORMULA :: MixResolve M_FORMULA
resolveM_FORMULA ga ids cf = case cf of
   BoxOrDiamond b m f ps -> do
       nm <- resolveMODALITY ga ids m
       nf <- resolveMixFrm mapM_FORMULA resolveM_FORMULA ga ids f
       return $ BoxOrDiamond b nm nf ps

minExpForm :: Min M_FORMULA ModalSign
minExpForm s form =
    let minMod md ps = case md of
                  Simple_mod i -> minMod (Term_mod (Mixfix_token i)) ps
                  Term_mod t -> let
                    r = do
                      t2 <- oneExpTerm minExpForm s t
                      let srt = sortOfTerm t2
                          trm = Term_mod t2
                          supers = supersortsOf srt s
                      if Set.null $ Set.intersection
                        (Set.insert srt supers)
                         $ Map.keysSet $ termModies $ extendedInfo s
                         then Result [mkDiag Error
                              ("unknown term modality sort '"
                               ++ showId srt "' for term") t ]
                              $ Just trm
                         else return trm
                    in case t of
                       Mixfix_token tm ->
                           if Map.member tm (modies $ extendedInfo s)
                              || tokStr tm == emptyS
                              then return $ Simple_mod tm
                              else Result
                                      [mkDiag Error "unknown modality" tm]
                                      $ Just $ Simple_mod tm
                       Application (Op_name (Id [tm] [] _)) [] _ ->
                           if Map.member tm (modies $ extendedInfo s)
                           then return $ Simple_mod tm
                           else r
                       _ -> r
    in case form of
        BoxOrDiamond b m f ps ->
            do nm <- minMod m ps
               f2 <- minExpFORMULA minExpForm s f
               return $ BoxOrDiamond b nm f2 ps

ana_M_SIG_ITEM :: Ana M_SIG_ITEM M_BASIC_ITEM M_SIG_ITEM M_FORMULA ModalSign
ana_M_SIG_ITEM mix mi =
    case mi of
    Rigid_op_items r al ps ->
        do ul <- mapM (ana_OP_ITEM minExpForm mix) al
           case r of
               Flexible -> mapM_ (\ aoi -> case item aoi of
                   Op_decl ops ty _ _ ->
                       mapM_ (updateExtInfo . addFlexOp (toOpType ty)) ops
                   Op_defn i par _ _ -> maybe (return ())
                       (\ ty -> updateExtInfo $ addFlexOp (toOpType ty) i)
                       $ headToType par) ul
               Rigid -> return ()
           return $ Rigid_op_items r ul ps
    Rigid_pred_items r al ps ->
        do ul <- mapM (ana_PRED_ITEM minExpForm mix) al
           case r of
               Flexible -> mapM_ (\ aoi -> case item aoi of
                   Pred_decl ops ty _ ->
                       mapM_ (updateExtInfo . addFlexPred (toPredType ty)) ops
                   Pred_defn i (Pred_head args _) _ _ ->
                       updateExtInfo $ addFlexPred
                                (PredType $ sortsOfArgs args) i ) ul
               Rigid -> return ()
           return $ Rigid_pred_items r ul ps

addFlexOp :: OpType -> Id -> ModalSign -> Result ModalSign
addFlexOp ty i m = return
       m { flexOps = addOpTo i ty $ flexOps m }

addFlexPred :: PredType -> Id -> ModalSign -> Result ModalSign
addFlexPred ty i m = return
       m { flexPreds = MapSet.insert i ty $ flexPreds m }

ana_M_BASIC_ITEM
    :: Ana M_BASIC_ITEM M_BASIC_ITEM M_SIG_ITEM M_FORMULA ModalSign
ana_M_BASIC_ITEM mix bi = case bi of
        Simple_mod_decl al fs ps -> do
            mapM_ ((updateExtInfo . preAddModId) . item) al
            newFs <- mapAnM (ana_FORMULA mix) fs
            resFs <- mapAnM (return . fst) newFs
            anaFs <- mapAnM (return . snd) newFs
            mapM_ ((updateExtInfo . addModId anaFs) . item) al
            return $ Simple_mod_decl al resFs ps
        Term_mod_decl al fs ps -> do
            e <- get
            mapM_ ((updateExtInfo . preAddModSort e) . item) al
            newFs <- mapAnM (ana_FORMULA mix) fs
            resFs <- mapAnM (return . fst) newFs
            anaFs <- mapAnM (return . snd) newFs
            mapM_ ((updateExtInfo . addModSort anaFs) . item) al
            return $ Term_mod_decl al resFs ps

preAddModId :: SIMPLE_ID -> ModalSign -> Result ModalSign
preAddModId i m =
    let ms = modies m in
    if Map.member i ms then
       Result [mkDiag Hint "repeated modality" i] $ Just m
       else return m { modies = Map.insert i [] ms }

addModId :: [AnModFORM] -> SIMPLE_ID -> ModalSign -> Result ModalSign
addModId frms i m = return m
  { modies = Map.insertWith List.union i frms $ modies m }

preAddModSort :: Sign M_FORMULA ModalSign -> SORT -> ModalSign
              -> Result ModalSign
preAddModSort e i m =
    let ms = termModies m
        ds = hasSort e i
    in if Map.member i ms || not (null ds) then
       Result (mkDiag Hint "repeated term modality" i : ds) $ Just m
       else return m { termModies = Map.insert i [] ms }

addModSort :: [AnModFORM] -> SORT -> ModalSign -> Result ModalSign
addModSort frms i m = return m
  { termModies = Map.insertWith List.union i frms $ termModies m }

ana_FORMULA :: Mix M_BASIC_ITEM M_SIG_ITEM M_FORMULA ModalSign
            -> FORMULA M_FORMULA -> State (Sign M_FORMULA ModalSign)
               (FORMULA M_FORMULA, FORMULA M_FORMULA)
ana_FORMULA mix f = do
           let ps = map simpleIdToId $ Set.toList $ getFormPredToks f
           pm <- gets predMap
           mapM_ (addPred (emptyAnno ()) $ PredType []) ps
           newGa <- gets globAnnos
           let Result es m = resolveFormula mapM_FORMULA
                             resolveM_FORMULA newGa (mixRules mix) f
           addDiags es
           e <- get
           phi <- case m of
               Nothing -> return (f, f)
               Just r -> do
                   n <- resultToState (minExpFORMULA minExpForm e) r
                   return (r, n)
           e2 <- get
           put e2 {predMap = pm}
           return phi

getFormPredToks :: FORMULA M_FORMULA -> Set.Set Token
getFormPredToks frm = case frm of
    Quantification _ _ f _ -> getFormPredToks f
    Junction _ fs _ -> Set.unions $ map getFormPredToks fs
    Relation f1 _ f2 _ -> on Set.union getFormPredToks f1 f2
    Negation f _ -> getFormPredToks f
    Mixfix_formula (Mixfix_token t) -> Set.singleton t
    Mixfix_formula t -> getTermPredToks t
    ExtFORMULA (BoxOrDiamond _ _ f _) -> getFormPredToks f
    Predication _ ts _ -> Set.unions $ map getTermPredToks ts
    Definedness t _ -> getTermPredToks t
    Equation t1 _ t2 _ -> on Set.union getTermPredToks t1 t2
    Membership t _ _ -> getTermPredToks t
    _ -> Set.empty

getTermPredToks :: TERM M_FORMULA -> Set.Set Token
getTermPredToks trm = case trm of
    Application _ ts _ -> Set.unions $ map getTermPredToks ts
    Sorted_term t _ _ -> getTermPredToks t
    Cast t _ _ -> getTermPredToks t
    Conditional t1 f t2 _ -> Set.union (getTermPredToks t1) $
        Set.union (getFormPredToks f) $ getTermPredToks t2
    Mixfix_term ts -> Set.unions $ map getTermPredToks ts
    Mixfix_parenthesized ts _ -> Set.unions $ map getTermPredToks ts
    Mixfix_bracketed ts _ -> Set.unions $ map getTermPredToks ts
    Mixfix_braced ts _ -> Set.unions $ map getTermPredToks ts
    _ -> Set.empty
