7d602f039beb26151cdc6306cfd3952b98bdc424jeff.schenkDescription : sublogic analysis for CoCASL
7d602f039beb26151cdc6306cfd3952b98bdc424jeff.schenkCopyright : (c) Till Mossakowski, C.Maeder and Uni Bremen 2002-2006
7d602f039beb26151cdc6306cfd3952b98bdc424jeff.schenkLicense : GPLv2 or higher, see LICENSE.txt
7d602f039beb26151cdc6306cfd3952b98bdc424jeff.schenkMaintainer : Christian.Maeder@dfki.de
7d602f039beb26151cdc6306cfd3952b98bdc424jeff.schenkStability : experimental
7d602f039beb26151cdc6306cfd3952b98bdc424jeff.schenkPortability : portable
7d602f039beb26151cdc6306cfd3952b98bdc424jeff.schenkThis module provides the sublogic functions (as required by Logic.hs)
7d602f039beb26151cdc6306cfd3952b98bdc424jeff.schenk for CoCASL. It is based on the respective functions for CASL.
7d602f039beb26151cdc6306cfd3952b98bdc424jeff.schenk ( CoCASL_Sublogics
7d602f039beb26151cdc6306cfd3952b98bdc424jeff.schenk , minFormSublogic
7d602f039beb26151cdc6306cfd3952b98bdc424jeff.schenk , minCSigItem
7d602f039beb26151cdc6306cfd3952b98bdc424jeff.schenk , minCBaseItem
7d602f039beb26151cdc6306cfd3952b98bdc424jeff.schenk , hasCoFeature
7d602f039beb26151cdc6306cfd3952b98bdc424jeff.schenk , setCoFeature
7d602f039beb26151cdc6306cfd3952b98bdc424jeff.schenk-- | type for CoCASL sublogics
7d602f039beb26151cdc6306cfd3952b98bdc424jeff.schenktype CoCASL_Sublogics = CASL_SL Bool
7d602f039beb26151cdc6306cfd3952b98bdc424jeff.schenkhasCoFeature :: CoCASL_Sublogics -> Bool
7d602f039beb26151cdc6306cfd3952b98bdc424jeff.schenkhasCoFeature = ext_features
7d602f039beb26151cdc6306cfd3952b98bdc424jeff.schenksetCoFeature :: Bool -> CoCASL_Sublogics -> CoCASL_Sublogics
7d602f039beb26151cdc6306cfd3952b98bdc424jeff.schenksetCoFeature b s = s { ext_features = b }
7d602f039beb26151cdc6306cfd3952b98bdc424jeff.schenktheCoFeature :: CoCASL_Sublogics
7d602f039beb26151cdc6306cfd3952b98bdc424jeff.schenktheCoFeature = setCoFeature True bottom
7d602f039beb26151cdc6306cfd3952b98bdc424jeff.schenkminFormSublogic :: C_FORMULA -> CoCASL_Sublogics
7d602f039beb26151cdc6306cfd3952b98bdc424jeff.schenkminFormSublogic cf = case cf of
7d602f039beb26151cdc6306cfd3952b98bdc424jeff.schenk BoxOrDiamond _ _ f _ ->
7d602f039beb26151cdc6306cfd3952b98bdc424jeff.schenk sublogics_max theCoFeature $ sl_sentence minFormSublogic f
7d602f039beb26151cdc6306cfd3952b98bdc424jeff.schenk CoSort_gen_ax {} -> theCoFeature
7d602f039beb26151cdc6306cfd3952b98bdc424jeff.schenk {- may be changed to Constraints with mappings
7d602f039beb26151cdc6306cfd3952b98bdc424jeff.schenk may be ops need to be checked for partiality? -}
7d602f039beb26151cdc6306cfd3952b98bdc424jeff.schenkminCSigItem :: C_SIG_ITEM -> CoCASL_Sublogics
7d602f039beb26151cdc6306cfd3952b98bdc424jeff.schenkminCSigItem (CoDatatype_items l _) =
7d602f039beb26151cdc6306cfd3952b98bdc424jeff.schenk foldl sublogics_max theCoFeature $ map (minCoDatatype . item) l
7d602f039beb26151cdc6306cfd3952b98bdc424jeff.schenkminCoDatatype :: CODATATYPE_DECL -> CoCASL_Sublogics
7d602f039beb26151cdc6306cfd3952b98bdc424jeff.schenkminCoDatatype (CoDatatype_decl _ l _) =
7d602f039beb26151cdc6306cfd3952b98bdc424jeff.schenk foldl sublogics_max theCoFeature $ map (minCoAlternative . item) l
7d602f039beb26151cdc6306cfd3952b98bdc424jeff.schenkminCoAlternative :: COALTERNATIVE -> CoCASL_Sublogics
7d602f039beb26151cdc6306cfd3952b98bdc424jeff.schenkminCoAlternative a = case a of
7d602f039beb26151cdc6306cfd3952b98bdc424jeff.schenk Co_construct fk _ l _ ->
7d602f039beb26151cdc6306cfd3952b98bdc424jeff.schenk foldl sublogics_max (sl_opkind fk) $ map minCoComponents l
7d602f039beb26151cdc6306cfd3952b98bdc424jeff.schenk CoSubsorts _ _ -> need_sub
7d602f039beb26151cdc6306cfd3952b98bdc424jeff.schenkminCoComponents :: COCOMPONENTS -> CoCASL_Sublogics
7d602f039beb26151cdc6306cfd3952b98bdc424jeff.schenkminCoComponents (CoSelect _ t _) = sl_op_type t
7d602f039beb26151cdc6306cfd3952b98bdc424jeff.schenkminCBaseItem :: C_BASIC_ITEM -> CoCASL_Sublogics
7d602f039beb26151cdc6306cfd3952b98bdc424jeff.schenkminCBaseItem bi = case bi of
7d602f039beb26151cdc6306cfd3952b98bdc424jeff.schenk CoFree_datatype l _ ->
7d602f039beb26151cdc6306cfd3952b98bdc424jeff.schenk foldl sublogics_max theCoFeature $ map (minCoDatatype . item) l
7d602f039beb26151cdc6306cfd3952b98bdc424jeff.schenk CoSort_gen l _ -> foldl sublogics_max theCoFeature $
7d602f039beb26151cdc6306cfd3952b98bdc424jeff.schenk map (sl_sig_items minCSigItem minFormSublogic . item) l