{- |
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 :: CoCASL_Sublogics -> Bool
hasCoFeature = CoCASL_Sublogics -> Bool
forall a. CASL_SL a -> a
ext_features

setCoFeature :: Bool -> CoCASL_Sublogics -> CoCASL_Sublogics
setCoFeature :: Bool -> CoCASL_Sublogics -> CoCASL_Sublogics
setCoFeature b :: Bool
b s :: CoCASL_Sublogics
s = CoCASL_Sublogics
s { ext_features :: Bool
ext_features = Bool
b }

theCoFeature :: CoCASL_Sublogics
theCoFeature :: CoCASL_Sublogics
theCoFeature = Bool -> CoCASL_Sublogics -> CoCASL_Sublogics
setCoFeature Bool
True CoCASL_Sublogics
forall a. Lattice a => CASL_SL a
bottom

minFormSublogic :: C_FORMULA -> CoCASL_Sublogics
minFormSublogic :: C_FORMULA -> CoCASL_Sublogics
minFormSublogic cf :: C_FORMULA
cf = case C_FORMULA
cf of
    BoxOrDiamond _ _ f :: FORMULA C_FORMULA
f _ ->
        CoCASL_Sublogics -> CoCASL_Sublogics -> CoCASL_Sublogics
forall a. Lattice a => CASL_SL a -> CASL_SL a -> CASL_SL a
sublogics_max CoCASL_Sublogics
theCoFeature (CoCASL_Sublogics -> CoCASL_Sublogics)
-> CoCASL_Sublogics -> CoCASL_Sublogics
forall a b. (a -> b) -> a -> b
$ (C_FORMULA -> CoCASL_Sublogics)
-> FORMULA C_FORMULA -> CoCASL_Sublogics
forall a f. Lattice a => (f -> CASL_SL a) -> FORMULA f -> CASL_SL a
sl_sentence C_FORMULA -> CoCASL_Sublogics
minFormSublogic FORMULA C_FORMULA
f
    CoSort_gen_ax {} -> CoCASL_Sublogics
theCoFeature
        {- may be changed to Constraints with mappings
        may be ops need to be checked for partiality? -}

minCSigItem :: C_SIG_ITEM -> CoCASL_Sublogics
minCSigItem :: C_SIG_ITEM -> CoCASL_Sublogics
minCSigItem (CoDatatype_items l :: [Annoted CODATATYPE_DECL]
l _) =
    (CoCASL_Sublogics -> CoCASL_Sublogics -> CoCASL_Sublogics)
-> CoCASL_Sublogics -> [CoCASL_Sublogics] -> CoCASL_Sublogics
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl CoCASL_Sublogics -> CoCASL_Sublogics -> CoCASL_Sublogics
forall a. Lattice a => CASL_SL a -> CASL_SL a -> CASL_SL a
sublogics_max CoCASL_Sublogics
theCoFeature ([CoCASL_Sublogics] -> CoCASL_Sublogics)
-> [CoCASL_Sublogics] -> CoCASL_Sublogics
forall a b. (a -> b) -> a -> b
$ (Annoted CODATATYPE_DECL -> CoCASL_Sublogics)
-> [Annoted CODATATYPE_DECL] -> [CoCASL_Sublogics]
forall a b. (a -> b) -> [a] -> [b]
map (CODATATYPE_DECL -> CoCASL_Sublogics
minCoDatatype (CODATATYPE_DECL -> CoCASL_Sublogics)
-> (Annoted CODATATYPE_DECL -> CODATATYPE_DECL)
-> Annoted CODATATYPE_DECL
-> CoCASL_Sublogics
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Annoted CODATATYPE_DECL -> CODATATYPE_DECL
forall a. Annoted a -> a
item) [Annoted CODATATYPE_DECL]
l

minCoDatatype :: CODATATYPE_DECL -> CoCASL_Sublogics
minCoDatatype :: CODATATYPE_DECL -> CoCASL_Sublogics
minCoDatatype (CoDatatype_decl _ l :: [Annoted COALTERNATIVE]
l _) =
    (CoCASL_Sublogics -> CoCASL_Sublogics -> CoCASL_Sublogics)
-> CoCASL_Sublogics -> [CoCASL_Sublogics] -> CoCASL_Sublogics
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl CoCASL_Sublogics -> CoCASL_Sublogics -> CoCASL_Sublogics
forall a. Lattice a => CASL_SL a -> CASL_SL a -> CASL_SL a
sublogics_max CoCASL_Sublogics
theCoFeature ([CoCASL_Sublogics] -> CoCASL_Sublogics)
-> [CoCASL_Sublogics] -> CoCASL_Sublogics
forall a b. (a -> b) -> a -> b
$ (Annoted COALTERNATIVE -> CoCASL_Sublogics)
-> [Annoted COALTERNATIVE] -> [CoCASL_Sublogics]
forall a b. (a -> b) -> [a] -> [b]
map (COALTERNATIVE -> CoCASL_Sublogics
minCoAlternative (COALTERNATIVE -> CoCASL_Sublogics)
-> (Annoted COALTERNATIVE -> COALTERNATIVE)
-> Annoted COALTERNATIVE
-> CoCASL_Sublogics
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Annoted COALTERNATIVE -> COALTERNATIVE
forall a. Annoted a -> a
item) [Annoted COALTERNATIVE]
l

minCoAlternative :: COALTERNATIVE -> CoCASL_Sublogics
minCoAlternative :: COALTERNATIVE -> CoCASL_Sublogics
minCoAlternative a :: COALTERNATIVE
a = case COALTERNATIVE
a of
    Co_construct fk :: OpKind
fk _ l :: [COCOMPONENTS]
l _ ->
        (CoCASL_Sublogics -> CoCASL_Sublogics -> CoCASL_Sublogics)
-> CoCASL_Sublogics -> [CoCASL_Sublogics] -> CoCASL_Sublogics
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl CoCASL_Sublogics -> CoCASL_Sublogics -> CoCASL_Sublogics
forall a. Lattice a => CASL_SL a -> CASL_SL a -> CASL_SL a
sublogics_max (OpKind -> CoCASL_Sublogics
forall a. Lattice a => OpKind -> CASL_SL a
sl_opkind OpKind
fk) ([CoCASL_Sublogics] -> CoCASL_Sublogics)
-> [CoCASL_Sublogics] -> CoCASL_Sublogics
forall a b. (a -> b) -> a -> b
$ (COCOMPONENTS -> CoCASL_Sublogics)
-> [COCOMPONENTS] -> [CoCASL_Sublogics]
forall a b. (a -> b) -> [a] -> [b]
map COCOMPONENTS -> CoCASL_Sublogics
minCoComponents [COCOMPONENTS]
l
    CoSubsorts _ _ -> CoCASL_Sublogics
forall a. Lattice a => CASL_SL a
need_sub

minCoComponents :: COCOMPONENTS -> CoCASL_Sublogics
minCoComponents :: COCOMPONENTS -> CoCASL_Sublogics
minCoComponents (CoSelect _ t :: OP_TYPE
t _) = OP_TYPE -> CoCASL_Sublogics
forall a. Lattice a => OP_TYPE -> CASL_SL a
sl_op_type OP_TYPE
t

minCBaseItem :: C_BASIC_ITEM -> CoCASL_Sublogics
minCBaseItem :: C_BASIC_ITEM -> CoCASL_Sublogics
minCBaseItem bi :: C_BASIC_ITEM
bi = case C_BASIC_ITEM
bi of
     CoFree_datatype l :: [Annoted CODATATYPE_DECL]
l _ ->
         (CoCASL_Sublogics -> CoCASL_Sublogics -> CoCASL_Sublogics)
-> CoCASL_Sublogics -> [CoCASL_Sublogics] -> CoCASL_Sublogics
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl CoCASL_Sublogics -> CoCASL_Sublogics -> CoCASL_Sublogics
forall a. Lattice a => CASL_SL a -> CASL_SL a -> CASL_SL a
sublogics_max CoCASL_Sublogics
theCoFeature ([CoCASL_Sublogics] -> CoCASL_Sublogics)
-> [CoCASL_Sublogics] -> CoCASL_Sublogics
forall a b. (a -> b) -> a -> b
$ (Annoted CODATATYPE_DECL -> CoCASL_Sublogics)
-> [Annoted CODATATYPE_DECL] -> [CoCASL_Sublogics]
forall a b. (a -> b) -> [a] -> [b]
map (CODATATYPE_DECL -> CoCASL_Sublogics
minCoDatatype (CODATATYPE_DECL -> CoCASL_Sublogics)
-> (Annoted CODATATYPE_DECL -> CODATATYPE_DECL)
-> Annoted CODATATYPE_DECL
-> CoCASL_Sublogics
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Annoted CODATATYPE_DECL -> CODATATYPE_DECL
forall a. Annoted a -> a
item) [Annoted CODATATYPE_DECL]
l
     CoSort_gen l :: [Annoted (SIG_ITEMS C_SIG_ITEM C_FORMULA)]
l _ -> (CoCASL_Sublogics -> CoCASL_Sublogics -> CoCASL_Sublogics)
-> CoCASL_Sublogics -> [CoCASL_Sublogics] -> CoCASL_Sublogics
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl CoCASL_Sublogics -> CoCASL_Sublogics -> CoCASL_Sublogics
forall a. Lattice a => CASL_SL a -> CASL_SL a -> CASL_SL a
sublogics_max CoCASL_Sublogics
theCoFeature ([CoCASL_Sublogics] -> CoCASL_Sublogics)
-> [CoCASL_Sublogics] -> CoCASL_Sublogics
forall a b. (a -> b) -> a -> b
$
         (Annoted (SIG_ITEMS C_SIG_ITEM C_FORMULA) -> CoCASL_Sublogics)
-> [Annoted (SIG_ITEMS C_SIG_ITEM C_FORMULA)] -> [CoCASL_Sublogics]
forall a b. (a -> b) -> [a] -> [b]
map ((C_SIG_ITEM -> CoCASL_Sublogics)
-> (C_FORMULA -> CoCASL_Sublogics)
-> SIG_ITEMS C_SIG_ITEM C_FORMULA
-> CoCASL_Sublogics
forall a s f.
Lattice a =>
(s -> CASL_SL a) -> (f -> CASL_SL a) -> SIG_ITEMS s f -> CASL_SL a
sl_sig_items C_SIG_ITEM -> CoCASL_Sublogics
minCSigItem C_FORMULA -> CoCASL_Sublogics
minFormSublogic (SIG_ITEMS C_SIG_ITEM C_FORMULA -> CoCASL_Sublogics)
-> (Annoted (SIG_ITEMS C_SIG_ITEM C_FORMULA)
    -> SIG_ITEMS C_SIG_ITEM C_FORMULA)
-> Annoted (SIG_ITEMS C_SIG_ITEM C_FORMULA)
-> CoCASL_Sublogics
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Annoted (SIG_ITEMS C_SIG_ITEM C_FORMULA)
-> SIG_ITEMS C_SIG_ITEM C_FORMULA
forall a. Annoted a -> a
item) [Annoted (SIG_ITEMS C_SIG_ITEM C_FORMULA)]
l