content: {- |
  Module      :  ./CoCASL/Sublogic.hs
  Description :  sublogic analysis for CoCASL
  Copyright   :  (c) Till Mossakowski, C.Maeder and Uni Bremen 2002-2006
  License     :  GPLv2 or higher, see LICENSE.txt
  Maintainer  :  Christian.Maeder@dfki.de
  Stability   :  experimental
  Portability :  portable
  
  This module provides the sublogic functions (as required by Logic.hs)
    for CoCASL. It is based on the respective functions for CASL.
  -}
  
  module CoCASL.Sublogic
      ( CoCASL_Sublogics
      , minFormSublogic
      , minCSigItem
      , minCBaseItem
      , hasCoFeature
      , setCoFeature
      ) where
  
  import Common.AS_Annotation
  import CASL.Sublogic
  import CoCASL.AS_CoCASL
  
  -- | type for CoCASL sublogics
  type CoCASL_Sublogics = CASL_SL Bool
  
  hasCoFeature :: CoCASL_Sublogics -> Bool
  hasCoFeature = ext_features
  
  setCoFeature :: Bool -> CoCASL_Sublogics -> CoCASL_Sublogics
  setCoFeature b s = s { ext_features = b }
  
  theCoFeature :: CoCASL_Sublogics
  theCoFeature = setCoFeature True bottom
  
  minFormSublogic :: C_FORMULA -> CoCASL_Sublogics
  minFormSublogic cf = case cf of
      BoxOrDiamond _ _ f _ ->
          sublogics_max theCoFeature $ sl_sentence minFormSublogic f
      CoSort_gen_ax {} -> theCoFeature
          {- may be changed to Constraints with mappings
          may be ops need to be checked for partiality? -}
  
  minCSigItem :: C_SIG_ITEM -> CoCASL_Sublogics
  minCSigItem (CoDatatype_items l _) =
      foldl sublogics_max theCoFeature $ map (minCoDatatype . item) l
  
  minCoDatatype :: CODATATYPE_DECL -> CoCASL_Sublogics
  minCoDatatype (CoDatatype_decl _ l _) =
      foldl sublogics_max theCoFeature $ map (minCoAlternative . item) l
  
  minCoAlternative :: COALTERNATIVE -> CoCASL_Sublogics
  minCoAlternative a = case a of
      Co_construct fk _ l _ ->
          foldl sublogics_max (sl_opkind fk) $ map minCoComponents l
      CoSubsorts _ _ -> need_sub
  
  minCoComponents :: COCOMPONENTS -> CoCASL_Sublogics
  minCoComponents (CoSelect _ t _) = sl_op_type t
  
  minCBaseItem :: C_BASIC_ITEM -> CoCASL_Sublogics
  minCBaseItem bi = case bi of
       CoFree_datatype l _ ->
           foldl sublogics_max theCoFeature $ map (minCoDatatype . item) l
       CoSort_gen l _ -> foldl sublogics_max theCoFeature $
           map (sl_sig_items minCSigItem minFormSublogic . item) l
  