content: {- |
  Module      :  ./Modal/StatAna.hs
  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
  