content: {-# LANGUAGE DeriveDataTypeable #-}
  {- |
  Module      :  ./ExtModal/Sublogic.hs
  Description :  Sublogics for ExtModal logic
  Copyright   :  (c) DFKI 2012
  License     :  GPLv2 or higher, see LICENSE.txt
  
  Maintainer  :  Christian.Maeder@dfki.de
  Stability   :  experimental
  Portability :  portable
  
  Sublogics for ExtModal Logic
  -}
  
  module ExtModal.Sublogic where
  
  import CASL.AS_Basic_CASL
  import CASL.Sublogic
  
  import Common.AS_Annotation
  
  import Data.Data
  import Data.Function
  import Data.List
  import qualified Data.Set as Set
  
  import ExtModal.AS_ExtModal
  import ExtModal.ExtModalSign
  
  data Frequency = None | One | Many
    deriving (Show, Eq, Ord, Enum, Typeable, Data)
  
  data Sublogic = Sublogic
      { hasModalities :: Frequency
      , hasTermMods :: Bool
      , hasTransClos :: Bool
      , hasNominals :: Bool
      , hasTimeMods :: Frequency
      , hasFixPoints :: Bool
      , hasFrameAxioms :: Bool
      } deriving (Show, Eq, Ord, Typeable, Data)
  
  maxSublogic :: Sublogic
  maxSublogic = Sublogic
      { hasModalities = Many
      , hasTermMods = True
      , hasTransClos = True
      , hasNominals = True
      , hasTimeMods = Many
      , hasFixPoints = True
      , hasFrameAxioms = True
      }
  
  botSublogic :: Sublogic
  botSublogic = Sublogic
      { hasModalities = None
      , hasTermMods = False
      , hasTransClos = False
      , hasNominals = False
      , hasTimeMods = None
      , hasFixPoints = False
      , hasFrameAxioms = False
      }
  
  -- | the sublogic that can be translated to FOL
  foleml :: Sublogic
  foleml = maxSublogic
    { hasTimeMods = None
    , hasFixPoints = False
    , hasTransClos = False
    , hasFrameAxioms = False
    }
  
  joinSublogic :: Sublogic -> Sublogic -> Sublogic
  joinSublogic a b =
    let onMax f = on max f a b
        termM = onMax hasTermMods
        timeM = onMax hasTimeMods
    in Sublogic
      { hasModalities = minMod termM timeM
          `max` onMax hasModalities
      , hasTermMods = termM
      , hasTransClos = onMax hasTransClos
      , hasNominals = onMax hasNominals
      , hasTimeMods = timeM
      , hasFixPoints = onMax hasFixPoints
      , hasFrameAxioms = onMax hasFrameAxioms
      }
  
  instance Lattice Sublogic where
    cjoin = joinSublogic
    ctop = maxSublogic
    bot = botSublogic
  
  joinSublogics :: [Sublogic] -> Sublogic
  joinSublogics = foldr joinSublogic botSublogic
  
  type ExtModalSL = CASL_SL Sublogic
  
  minSublogicOfForm :: FORMULA EM_FORMULA -> ExtModalSL
  minSublogicOfForm = sl_sentence minSublogicOfEM
  
  minSublogicOfTerm :: TERM EM_FORMULA -> ExtModalSL
  minSublogicOfTerm = sl_term minSublogicOfEM
  
  minSublogicOfMod :: MODALITY -> ExtModalSL
  minSublogicOfMod m = case m of
      SimpleMod _ -> bottom
      TermMod t -> minSublogicOfTerm t
      ModOp _ m1 m2 -> on sublogics_max minSublogicOfMod m1 m2
      TransClos c -> updExtFeature (\ s -> s {hasTransClos = True})
        (minSublogicOfMod c)
      Guard f -> minSublogicOfForm f
  
  minSublogicOfPrefix :: FormPrefix -> ExtModalSL
  minSublogicOfPrefix fp = case fp of
      BoxOrDiamond _ m _ _ -> minSublogicOfMod m
      Hybrid _ _ -> mkBot botSublogic {hasNominals = True}
      FixedPoint _ _ -> mkBot botSublogic {hasFixPoints = True}
      _ -> updExtFeature (setTimeMods True [()]) bottom
  
  minSublogicOfEM :: EM_FORMULA -> ExtModalSL
  minSublogicOfEM ef = case ef of
      PrefixForm pf f _ -> sublogics_max (minSublogicOfPrefix pf)
          (minSublogicOfForm f)
      UntilSince _ f1 f2 _ -> updExtFeature (setTimeMods True [()])
        $ on sublogics_max minSublogicOfForm f1 f2
      ModForm md -> minSublogicOfModDefn md
  
  minSublogicOfModDefn :: ModDefn -> ExtModalSL
  minSublogicOfModDefn (ModDefn time term il fl _) =
      updExtFeature (\ s -> s {hasFrameAxioms = not $ null fl})
      . updExtFeature (setModalities il)
      . updExtFeature (setTermMods term)
      . updExtFeature (setTimeMods time il)
      . comp_list . map (minSublogicOfForm . item)
            $ concatMap (frameForms . item) fl
  
  minSublogicEMSign :: EModalSign -> ExtModalSL
  minSublogicEMSign s = mkBot botSublogic
    { hasTermMods = not . Set.null $ termMods s
    , hasTimeMods = case Set.size $ timeMods s of
        0 -> None
        1 -> One
        _ -> Many
    , hasNominals = not . Set.null $ nominals s
    , hasModalities = case Set.size $ modalities s of
        0 -> None
        1 -> One
        _ -> Many
    }
  
  minSublogicEMBasic :: EM_BASIC_ITEM -> ExtModalSL
  minSublogicEMBasic bi = case bi of
    ModItem md -> minSublogicOfModDefn md
    Nominal_decl l _ -> mkBot botSublogic { hasNominals = not $ null l }
  
  minSLExtSigItem :: EM_SIG_ITEM -> [ExtModalSL]
  minSLExtSigItem si = case si of
    Rigid_op_items _ os _ -> map (sl_op_item minSublogicOfEM . item) os
    Rigid_pred_items _ ps _ -> map (sl_pred_item minSublogicOfEM . item) ps
  
  setModalities :: [a] -> Sublogic -> Sublogic
  setModalities il s = case il of
      [_] -> s {hasModalities = max One (hasModalities s)}
      _ -> s {hasModalities = Many}
  
  setTermMods :: Bool -> Sublogic -> Sublogic
  setTermMods b s = if b then s {hasTermMods = True} else s
  
  setTimeMods :: Bool -> [a] -> Sublogic -> Sublogic
  setTimeMods b il s = if b then case il of
      [_] -> s {hasTimeMods = max One (hasTimeMods s)}
      _ -> s {hasTimeMods = Many}
      else s
  
  minMod :: Bool -> Frequency -> Frequency
  minMod h_term h_time = if h_term && h_time == None then One
    else h_time
  
  sublogicsDim :: [[Sublogic]]
  sublogicsDim = let
    t = True
    b = bot
    f = [One, Many]
    in [ [ b { hasModalities = h } | h <- f]
       , [ b { hasTermMods = t }]
       , [ b { hasTransClos = t }]
       , [ b { hasNominals = t }]
       , [ b { hasModalities = h } | h <- f]
       , [ b { hasFixPoints = t }]
       , [ b { hasFrameAxioms = t }] ]
  
  sublogName :: Sublogic -> String
  sublogName s = (if hasModalities s == Many then "Many" else "One")
      ++ (if hasTermMods s then "Dyn" else "")
      ++ (if hasNominals s then "Hybr" else "")
      ++ (if hasTimeMods s == Many then "Time"
         else if hasTimeMods s == One then "SingleTime" else "")
      ++ (if hasFixPoints s then "Fix" else "")
      ++ (if hasFrameAxioms s then "Frames" else "")
      ++ if hasTransClos s then "*" else ""
  
  parseSublog :: String -> (Sublogic, String)
  parseSublog s0 = let
    (m, s1) = case stripPrefix "Many" s0 of
      Nothing -> case stripPrefix "One" s0 of
        Nothing -> (None, s0)
        Just r -> (One, r)
      Just r -> (Many, r)
    (tm, s2) = parseBool "Dyn" s1
    (n, s3) = parseBool "Hybr" s2
    (ti, s4) = case stripPrefix "Time" s3 of
      Just r -> (Many, r)
      Nothing -> case stripPrefix "SingleTime" s3 of
        Nothing -> (None, s3)
        Just r -> (One, r)
    (fi, s5) = parseBool "Fix" s4
    (fr, s6) = parseBool "Frames" s5
    (tr, s7) = parseBool "*" s6
    in (Sublogic
      { hasModalities = max m $ minMod tm ti
      , hasTermMods = tm
      , hasTransClos = tr
      , hasNominals = n
      , hasTimeMods = ti
      , hasFixPoints = fi
      , hasFrameAxioms = fr
      }, s7)
  