{- |

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