Sublogic.hs revision ea8e98e298f33f9362293f392c8fb192722b8904
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiuModule : $Header$
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiuDescription : sublogic analysis for CoCASL
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiuCopyright : (c) Till Mossakowski, C.Maeder and Uni Bremen 2002-2006
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiuLicense : GPLv2 or higher, see LICENSE.txt
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiuMaintainer : Christian.Maeder@dfki.de
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiuStability : experimental
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiuPortability : portable
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiuThis module provides the sublogic functions (as required by Logic.hs)
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu for CoCASL. It is based on the respective functions for CASL.
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu ( CoCASL_Sublogics
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu , minFormSublogic
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu-- | type for CoCASL sublogics
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiutype CoCASL_Sublogics = CASL_SL Bool
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiuhasCoFeature :: CoCASL_Sublogics -> Bool
a604cbad8e2202147b5c6bb9f2e06ae61162d654Felix Gabriel MancehasCoFeature = ext_features
be2439588008221e691321fdf4f75432cfb72878Felix Gabriel MancesetCoFeature :: Bool -> CoCASL_Sublogics -> CoCASL_Sublogics
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiusetCoFeature b s = s { ext_features = b }
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiutheCoFeature :: CoCASL_Sublogics
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiutheCoFeature = setCoFeature True bottom
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiuminFormSublogic :: C_FORMULA -> CoCASL_Sublogics
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiuminFormSublogic cf = case cf of
e0f1794e365dd347e97b37d7d22b2fce27296fa1Christian Maeder BoxOrDiamond _ _ f _ ->
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu sublogics_max theCoFeature $ sl_sentence minFormSublogic f
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu CoSort_gen_ax _ _ _ -> theCoFeature
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu -- may be changed to Constraints with mappings
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu -- may be ops need to be checked for partiality?
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiuminCSigItem :: C_SIG_ITEM -> CoCASL_Sublogics
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiuminCSigItem (CoDatatype_items l _) =
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu foldl sublogics_max theCoFeature $ map (minCoDatatype . item) l
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiuminCoDatatype :: CODATATYPE_DECL -> CoCASL_Sublogics
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiuminCoDatatype (CoDatatype_decl _ l _) =
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu foldl sublogics_max theCoFeature $ map (minCoAlternative . item) l
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiuminCoAlternative :: COALTERNATIVE -> CoCASL_Sublogics
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiuminCoAlternative a = case a of
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu Co_construct fk _ l _ ->
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu foldl sublogics_max (sl_opkind fk) $ map minCoComponents l
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu CoSubsorts _ _ -> need_sub
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiuminCoComponents :: COCOMPONENTS -> CoCASL_Sublogics
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiuminCoComponents (CoSelect _ t _) = sl_op_type t
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiuminCBaseItem :: C_BASIC_ITEM -> CoCASL_Sublogics
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiuminCBaseItem bi = case bi of
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu CoFree_datatype l _ ->
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu foldl sublogics_max theCoFeature $ map minCoDatatype $ map item l
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu CoSort_gen l _ -> foldl sublogics_max theCoFeature $
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu map (sl_sig_items minCSigItem minFormSublogic . item) l