{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}
{- |
Module      :  ./CASL_DL/Logic_CASL_DL.hs
Description :  Instance of class Logic for CASL DL
Copyright   :  (c) Klaus Luettich, Uni Bremen 2005
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  luecke@informatik.uni-bremen.de
Stability   :  provisional
Portability :  portable

Instance of class Logic for CASL DL
-}

module CASL_DL.Logic_CASL_DL (CASL_DL (..), DLMor, DLFORMULA) where

import qualified Data.Set as Set
import qualified Common.Lib.Rel as Rel
import Common.Result
import Common.ProofTree
import Common.DocUtils

import CASL_DL.AS_CASL_DL
import CASL_DL.Sign
import CASL_DL.PredefinedCASLAxioms
import CASL_DL.ATC_CASL_DL ()
import CASL_DL.Parse_AS ()
import CASL_DL.StatAna

import CASL.Sign
import CASL.Morphism
import CASL.SymbolMapAnalysis
import CASL.AS_Basic_CASL
import CASL.Parse_AS_Basic
import CASL.MapSentence
import CASL.SymbolParser
import CASL.Taxonomy
import CASL.SimplifySen
import CASL.Logic_CASL ()
import CASL_DL.Sublogics

import Logic.Logic

data CASL_DL = CASL_DL deriving Int -> CASL_DL -> ShowS
[CASL_DL] -> ShowS
CASL_DL -> String
(Int -> CASL_DL -> ShowS)
-> (CASL_DL -> String) -> ([CASL_DL] -> ShowS) -> Show CASL_DL
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [CASL_DL] -> ShowS
$cshowList :: [CASL_DL] -> ShowS
show :: CASL_DL -> String
$cshow :: CASL_DL -> String
showsPrec :: Int -> CASL_DL -> ShowS
$cshowsPrec :: Int -> CASL_DL -> ShowS
Show

instance Language CASL_DL where
 description :: CASL_DL -> String
description _ = [String] -> String
unlines
  [ "CASL_DL is the restriction of CASL to OWL 1 expressivity."
  , "It additionally provides cardinality restrictions in a description logic"
  , "sense; and it limits the expressivity of CASL to the description logic"
  , "SHOIN(D). Hence it provides the following sublogics:"
  , "  * Card -- CASL plus cardinality restrictions on binary relations"
  , "  * DL   -- SHOIN(D)"
  , "  * SHIQ"
  , "  * SHOIQ" ]

type DLMor = Morphism DL_FORMULA CASL_DLSign (DefMorExt CASL_DLSign)
type DLFORMULA = FORMULA DL_FORMULA

instance SignExtension CASL_DLSign where
  isSubSignExtension :: CASL_DLSign -> CASL_DLSign -> Bool
isSubSignExtension = CASL_DLSign -> CASL_DLSign -> Bool
isSubCASL_DLSign

instance Syntax CASL_DL DL_BASIC_SPEC
                Symbol SYMB_ITEMS SYMB_MAP_ITEMS
      where
         parse_basic_spec :: CASL_DL -> Maybe (PrefixMap -> AParser st DL_BASIC_SPEC)
parse_basic_spec CASL_DL = (PrefixMap -> AParser st DL_BASIC_SPEC)
-> Maybe (PrefixMap -> AParser st DL_BASIC_SPEC)
forall a. a -> Maybe a
Just ((PrefixMap -> AParser st DL_BASIC_SPEC)
 -> Maybe (PrefixMap -> AParser st DL_BASIC_SPEC))
-> (PrefixMap -> AParser st DL_BASIC_SPEC)
-> Maybe (PrefixMap -> AParser st DL_BASIC_SPEC)
forall a b. (a -> b) -> a -> b
$ [String] -> PrefixMap -> AParser st DL_BASIC_SPEC
forall f s b st.
(TermParser f, AParsable s, AParsable b) =>
[String] -> PrefixMap -> AParser st (BASIC_SPEC b s f)
basicSpec [String]
casl_DL_reserved_words
         parse_symb_items :: CASL_DL -> Maybe (PrefixMap -> AParser st SYMB_ITEMS)
parse_symb_items CASL_DL = (PrefixMap -> AParser st SYMB_ITEMS)
-> Maybe (PrefixMap -> AParser st SYMB_ITEMS)
forall a. a -> Maybe a
Just ((PrefixMap -> AParser st SYMB_ITEMS)
 -> Maybe (PrefixMap -> AParser st SYMB_ITEMS))
-> (AParser st SYMB_ITEMS -> PrefixMap -> AParser st SYMB_ITEMS)
-> AParser st SYMB_ITEMS
-> Maybe (PrefixMap -> AParser st SYMB_ITEMS)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AParser st SYMB_ITEMS -> PrefixMap -> AParser st SYMB_ITEMS
forall a b. a -> b -> a
const (AParser st SYMB_ITEMS
 -> Maybe (PrefixMap -> AParser st SYMB_ITEMS))
-> AParser st SYMB_ITEMS
-> Maybe (PrefixMap -> AParser st SYMB_ITEMS)
forall a b. (a -> b) -> a -> b
$ [String] -> AParser st SYMB_ITEMS
forall st. [String] -> AParser st SYMB_ITEMS
symbItems [String]
casl_DL_reserved_words
         parse_symb_map_items :: CASL_DL -> Maybe (PrefixMap -> AParser st SYMB_MAP_ITEMS)
parse_symb_map_items CASL_DL =
              (PrefixMap -> AParser st SYMB_MAP_ITEMS)
-> Maybe (PrefixMap -> AParser st SYMB_MAP_ITEMS)
forall a. a -> Maybe a
Just ((PrefixMap -> AParser st SYMB_MAP_ITEMS)
 -> Maybe (PrefixMap -> AParser st SYMB_MAP_ITEMS))
-> (AParser st SYMB_MAP_ITEMS
    -> PrefixMap -> AParser st SYMB_MAP_ITEMS)
-> AParser st SYMB_MAP_ITEMS
-> Maybe (PrefixMap -> AParser st SYMB_MAP_ITEMS)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AParser st SYMB_MAP_ITEMS -> PrefixMap -> AParser st SYMB_MAP_ITEMS
forall a b. a -> b -> a
const (AParser st SYMB_MAP_ITEMS
 -> Maybe (PrefixMap -> AParser st SYMB_MAP_ITEMS))
-> AParser st SYMB_MAP_ITEMS
-> Maybe (PrefixMap -> AParser st SYMB_MAP_ITEMS)
forall a b. (a -> b) -> a -> b
$ [String] -> AParser st SYMB_MAP_ITEMS
forall st. [String] -> AParser st SYMB_MAP_ITEMS
symbMapItems [String]
casl_DL_reserved_words

-- CASL_DL logic

map_DL_FORMULA :: MapSen DL_FORMULA CASL_DLSign (DefMorExt CASL_DLSign)
map_DL_FORMULA :: MapSen DL_FORMULA CASL_DLSign (DefMorExt CASL_DLSign)
map_DL_FORMULA mor :: Morphism DL_FORMULA CASL_DLSign (DefMorExt CASL_DLSign)
mor (Cardinality ct :: CardType
ct pn :: PRED_SYMB
pn varT :: TERM DL_FORMULA
varT natT :: TERM DL_FORMULA
natT qualT :: Maybe (FORMULA DL_FORMULA)
qualT r :: Range
r) =
    CardType
-> PRED_SYMB
-> TERM DL_FORMULA
-> TERM DL_FORMULA
-> Maybe (FORMULA DL_FORMULA)
-> Range
-> DL_FORMULA
Cardinality CardType
ct PRED_SYMB
pn' TERM DL_FORMULA
varT' TERM DL_FORMULA
natT' Maybe (FORMULA DL_FORMULA)
qualT Range
r
    where pn' :: PRED_SYMB
pn' = Morphism DL_FORMULA CASL_DLSign (DefMorExt CASL_DLSign)
-> PRED_SYMB -> PRED_SYMB
forall f e m. Morphism f e m -> PRED_SYMB -> PRED_SYMB
mapPrSymb Morphism DL_FORMULA CASL_DLSign (DefMorExt CASL_DLSign)
mor PRED_SYMB
pn
          varT' :: TERM DL_FORMULA
varT' = TERM DL_FORMULA -> TERM DL_FORMULA
mapTrm TERM DL_FORMULA
varT
          natT' :: TERM DL_FORMULA
natT' = TERM DL_FORMULA -> TERM DL_FORMULA
mapTrm TERM DL_FORMULA
natT
          mapTrm :: TERM DL_FORMULA -> TERM DL_FORMULA
mapTrm = MapSen DL_FORMULA CASL_DLSign (DefMorExt CASL_DLSign)
-> Morphism DL_FORMULA CASL_DLSign (DefMorExt CASL_DLSign)
-> TERM DL_FORMULA
-> TERM DL_FORMULA
forall f e m. MapSen f e m -> Morphism f e m -> TERM f -> TERM f
mapTerm MapSen DL_FORMULA CASL_DLSign (DefMorExt CASL_DLSign)
map_DL_FORMULA Morphism DL_FORMULA CASL_DLSign (DefMorExt CASL_DLSign)
mor

instance Sentences CASL_DL DLFORMULA DLSign DLMor Symbol where
      map_sen :: CASL_DL
-> Morphism DL_FORMULA CASL_DLSign (DefMorExt CASL_DLSign)
-> FORMULA DL_FORMULA
-> Result (FORMULA DL_FORMULA)
map_sen CASL_DL m :: Morphism DL_FORMULA CASL_DLSign (DefMorExt CASL_DLSign)
m = FORMULA DL_FORMULA -> Result (FORMULA DL_FORMULA)
forall (m :: * -> *) a. Monad m => a -> m a
return (FORMULA DL_FORMULA -> Result (FORMULA DL_FORMULA))
-> (FORMULA DL_FORMULA -> FORMULA DL_FORMULA)
-> FORMULA DL_FORMULA
-> Result (FORMULA DL_FORMULA)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MapSen DL_FORMULA CASL_DLSign (DefMorExt CASL_DLSign)
-> Morphism DL_FORMULA CASL_DLSign (DefMorExt CASL_DLSign)
-> FORMULA DL_FORMULA
-> FORMULA DL_FORMULA
forall e m f.
MorphismExtension e m =>
MapSen f e m -> Morphism f e m -> FORMULA f -> FORMULA f
mapSen MapSen DL_FORMULA CASL_DLSign (DefMorExt CASL_DLSign)
map_DL_FORMULA Morphism DL_FORMULA CASL_DLSign (DefMorExt CASL_DLSign)
m
      sym_of :: CASL_DL -> DLSign -> [Set Symbol]
sym_of CASL_DL = DLSign -> [Set Symbol]
forall f e. Sign f e -> [Set Symbol]
symOf
      symKind :: CASL_DL -> Symbol -> String
symKind CASL_DL = Doc -> String
forall a. Show a => a -> String
show (Doc -> String) -> (Symbol -> Doc) -> Symbol -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SYMB_KIND -> Doc
forall a. Pretty a => a -> Doc
pretty (SYMB_KIND -> Doc) -> (Symbol -> SYMB_KIND) -> Symbol -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SymbType -> SYMB_KIND
symbolKind (SymbType -> SYMB_KIND)
-> (Symbol -> SymbType) -> Symbol -> SYMB_KIND
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> SymbType
symbType
      symmap_of :: CASL_DL
-> Morphism DL_FORMULA CASL_DLSign (DefMorExt CASL_DLSign)
-> EndoMap Symbol
symmap_of CASL_DL = Morphism DL_FORMULA CASL_DLSign (DefMorExt CASL_DLSign)
-> EndoMap Symbol
forall f e m. Morphism f e m -> EndoMap Symbol
morphismToSymbMap
      sym_name :: CASL_DL -> Symbol -> Id
sym_name CASL_DL = Symbol -> Id
symName
      simplify_sen :: CASL_DL -> DLSign -> FORMULA DL_FORMULA -> FORMULA DL_FORMULA
simplify_sen CASL_DL = Min DL_FORMULA CASL_DLSign
-> (DLSign -> DL_FORMULA -> DL_FORMULA)
-> DLSign
-> FORMULA DL_FORMULA
-> FORMULA DL_FORMULA
forall f e.
(FormExtension f, TermExtension f) =>
Min f e
-> (Sign f e -> f -> f) -> Sign f e -> FORMULA f -> FORMULA f
simplifySen Min DL_FORMULA CASL_DLSign
minDLForm DLSign -> DL_FORMULA -> DL_FORMULA
simplifyCD

simplifyCD :: DLSign -> DL_FORMULA -> DL_FORMULA
simplifyCD :: DLSign -> DL_FORMULA -> DL_FORMULA
simplifyCD sign :: DLSign
sign (Cardinality ct :: CardType
ct ps :: PRED_SYMB
ps t1 :: TERM DL_FORMULA
t1 t2 :: TERM DL_FORMULA
t2 t3 :: Maybe (FORMULA DL_FORMULA)
t3 r :: Range
r) = DL_FORMULA
simpCard
    where simpCard :: DL_FORMULA
simpCard = DL_FORMULA
-> (DL_FORMULA -> DL_FORMULA) -> Maybe DL_FORMULA -> DL_FORMULA
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (PRED_SYMB -> DL_FORMULA
card PRED_SYMB
ps)
                           (DL_FORMULA -> DL_FORMULA -> DL_FORMULA
forall a b. a -> b -> a
const (DL_FORMULA -> DL_FORMULA -> DL_FORMULA)
-> DL_FORMULA -> DL_FORMULA -> DL_FORMULA
forall a b. (a -> b) -> a -> b
$ PRED_SYMB -> DL_FORMULA
card (PRED_SYMB -> DL_FORMULA) -> PRED_SYMB -> DL_FORMULA
forall a b. (a -> b) -> a -> b
$ Id -> PRED_SYMB
Pred_name Id
pn)
                           (Result DL_FORMULA -> Maybe DL_FORMULA
forall a. Result a -> Maybe a
resultToMaybe (Result DL_FORMULA -> Maybe DL_FORMULA)
-> Result DL_FORMULA -> Maybe DL_FORMULA
forall a b. (a -> b) -> a -> b
$
                            Min DL_FORMULA CASL_DLSign
minDLForm DLSign
sign (DL_FORMULA -> Result DL_FORMULA)
-> DL_FORMULA -> Result DL_FORMULA
forall a b. (a -> b) -> a -> b
$ PRED_SYMB -> DL_FORMULA
card (PRED_SYMB -> DL_FORMULA) -> PRED_SYMB -> DL_FORMULA
forall a b. (a -> b) -> a -> b
$ Id -> PRED_SYMB
Pred_name Id
pn)
          simp :: TERM DL_FORMULA -> TERM DL_FORMULA
simp = Min DL_FORMULA CASL_DLSign
-> (DLSign -> DL_FORMULA -> DL_FORMULA)
-> DLSign
-> TERM DL_FORMULA
-> TERM DL_FORMULA
forall f e.
(FormExtension f, TermExtension f) =>
Min f e -> (Sign f e -> f -> f) -> Sign f e -> TERM f -> TERM f
rmTypesT Min DL_FORMULA CASL_DLSign
minDLForm DLSign -> DL_FORMULA -> DL_FORMULA
simplifyCD DLSign
sign
          card :: PRED_SYMB -> DL_FORMULA
card psy :: PRED_SYMB
psy = CardType
-> PRED_SYMB
-> TERM DL_FORMULA
-> TERM DL_FORMULA
-> Maybe (FORMULA DL_FORMULA)
-> Range
-> DL_FORMULA
Cardinality CardType
ct PRED_SYMB
psy (TERM DL_FORMULA -> TERM DL_FORMULA
simp TERM DL_FORMULA
t1) (TERM DL_FORMULA -> TERM DL_FORMULA
simp TERM DL_FORMULA
t2) Maybe (FORMULA DL_FORMULA)
t3 Range
r
          pn :: Id
pn = case PRED_SYMB
ps of
               Pred_name n :: Id
n -> Id
n
               Qual_pred_name n :: Id
n _pType :: PRED_TYPE
_pType _ -> Id
n

instance StaticAnalysis CASL_DL DL_BASIC_SPEC DLFORMULA
               SYMB_ITEMS SYMB_MAP_ITEMS
               DLSign
               DLMor
               Symbol RawSymbol where
         basic_analysis :: CASL_DL
-> Maybe
     ((DL_BASIC_SPEC, DLSign, GlobalAnnos)
      -> Result
           (DL_BASIC_SPEC, ExtSign DLSign Symbol,
            [Named (FORMULA DL_FORMULA)]))
basic_analysis CASL_DL = ((DL_BASIC_SPEC, DLSign, GlobalAnnos)
 -> Result
      (DL_BASIC_SPEC, ExtSign DLSign Symbol,
       [Named (FORMULA DL_FORMULA)]))
-> Maybe
     ((DL_BASIC_SPEC, DLSign, GlobalAnnos)
      -> Result
           (DL_BASIC_SPEC, ExtSign DLSign Symbol,
            [Named (FORMULA DL_FORMULA)]))
forall a. a -> Maybe a
Just (DL_BASIC_SPEC, DLSign, GlobalAnnos)
-> Result
     (DL_BASIC_SPEC, ExtSign DLSign Symbol,
      [Named (FORMULA DL_FORMULA)])
basicCASL_DLAnalysis
         stat_symb_map_items :: CASL_DL
-> DLSign
-> Maybe DLSign
-> [SYMB_MAP_ITEMS]
-> Result (EndoMap RawSymbol)
stat_symb_map_items CASL_DL s :: DLSign
s t :: Maybe DLSign
t sml :: [SYMB_MAP_ITEMS]
sml =
             DLSign
-> Maybe DLSign -> [SYMB_MAP_ITEMS] -> Result (EndoMap RawSymbol)
forall f e.
Sign f e
-> Maybe (Sign f e)
-> [SYMB_MAP_ITEMS]
-> Result (EndoMap RawSymbol)
statSymbMapItems DLSign
s Maybe DLSign
t [SYMB_MAP_ITEMS]
sml Result (EndoMap RawSymbol)
-> (EndoMap RawSymbol -> Result (EndoMap RawSymbol))
-> Result (EndoMap RawSymbol)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= EndoMap RawSymbol -> Result (EndoMap RawSymbol)
checkSymbolMapDL
         stat_symb_items :: CASL_DL -> DLSign -> [SYMB_ITEMS] -> Result [RawSymbol]
stat_symb_items CASL_DL = DLSign -> [SYMB_ITEMS] -> Result [RawSymbol]
forall f e. Sign f e -> [SYMB_ITEMS] -> Result [RawSymbol]
statSymbItems

         symbol_to_raw :: CASL_DL -> Symbol -> RawSymbol
symbol_to_raw CASL_DL = Symbol -> RawSymbol
symbolToRaw
         id_to_raw :: CASL_DL -> Id -> RawSymbol
id_to_raw CASL_DL = Id -> RawSymbol
idToRaw
         matches :: CASL_DL -> Symbol -> RawSymbol -> Bool
matches CASL_DL = Symbol -> RawSymbol -> Bool
CASL.Morphism.matches

         empty_signature :: CASL_DL -> DLSign
empty_signature CASL_DL = CASL_DLSign -> DLSign
forall e f. e -> Sign f e
emptySign CASL_DLSign
emptyCASL_DLSign
         signature_union :: CASL_DL -> DLSign -> DLSign -> Result DLSign
signature_union CASL_DL s :: DLSign
s = DLSign -> Result DLSign
forall (m :: * -> *) a. Monad m => a -> m a
return (DLSign -> Result DLSign)
-> (DLSign -> DLSign) -> DLSign -> Result DLSign
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (CASL_DLSign -> CASL_DLSign -> CASL_DLSign)
-> DLSign -> DLSign -> DLSign
forall e f. (e -> e -> e) -> Sign f e -> Sign f e -> Sign f e
addSig CASL_DLSign -> CASL_DLSign -> CASL_DLSign
addCASL_DLSign DLSign
s
         morphism_union :: CASL_DL
-> Morphism DL_FORMULA CASL_DLSign (DefMorExt CASL_DLSign)
-> Morphism DL_FORMULA CASL_DLSign (DefMorExt CASL_DLSign)
-> Result (Morphism DL_FORMULA CASL_DLSign (DefMorExt CASL_DLSign))
morphism_union CASL_DL = (CASL_DLSign -> CASL_DLSign -> CASL_DLSign)
-> Morphism DL_FORMULA CASL_DLSign (DefMorExt CASL_DLSign)
-> Morphism DL_FORMULA CASL_DLSign (DefMorExt CASL_DLSign)
-> Result (Morphism DL_FORMULA CASL_DLSign (DefMorExt CASL_DLSign))
forall e f m.
(e -> e -> e)
-> Morphism f e m -> Morphism f e m -> Result (Morphism f e m)
plainMorphismUnion CASL_DLSign -> CASL_DLSign -> CASL_DLSign
addCASL_DLSign
         final_union :: CASL_DL -> DLSign -> DLSign -> Result DLSign
final_union CASL_DL = (CASL_DLSign -> CASL_DLSign -> CASL_DLSign)
-> DLSign -> DLSign -> Result DLSign
forall e f.
(e -> e -> e) -> Sign f e -> Sign f e -> Result (Sign f e)
finalUnion CASL_DLSign -> CASL_DLSign -> CASL_DLSign
addCASL_DLSign
         is_subsig :: CASL_DL -> DLSign -> DLSign -> Bool
is_subsig CASL_DL = (CASL_DLSign -> CASL_DLSign -> Bool) -> DLSign -> DLSign -> Bool
forall e f. (e -> e -> Bool) -> Sign f e -> Sign f e -> Bool
isSubSig CASL_DLSign -> CASL_DLSign -> Bool
isSubCASL_DLSign
         subsig_inclusion :: CASL_DL
-> DLSign
-> DLSign
-> Result (Morphism DL_FORMULA CASL_DLSign (DefMorExt CASL_DLSign))
subsig_inclusion CASL_DL = DefMorExt CASL_DLSign
-> DLSign
-> DLSign
-> Result (Morphism DL_FORMULA CASL_DLSign (DefMorExt CASL_DLSign))
forall m f e. m -> Sign f e -> Sign f e -> Result (Morphism f e m)
sigInclusion DefMorExt CASL_DLSign
forall e. DefMorExt e
emptyMorExt
         cogenerated_sign :: CASL_DL
-> Set Symbol
-> DLSign
-> Result (Morphism DL_FORMULA CASL_DLSign (DefMorExt CASL_DLSign))
cogenerated_sign CASL_DL = DefMorExt CASL_DLSign
-> Set Symbol
-> DLSign
-> Result (Morphism DL_FORMULA CASL_DLSign (DefMorExt CASL_DLSign))
forall m f e.
m -> Set Symbol -> Sign f e -> Result (Morphism f e m)
cogeneratedSign DefMorExt CASL_DLSign
forall e. DefMorExt e
emptyMorExt
         generated_sign :: CASL_DL
-> Set Symbol
-> DLSign
-> Result (Morphism DL_FORMULA CASL_DLSign (DefMorExt CASL_DLSign))
generated_sign CASL_DL = DefMorExt CASL_DLSign
-> Set Symbol
-> DLSign
-> Result (Morphism DL_FORMULA CASL_DLSign (DefMorExt CASL_DLSign))
forall m f e.
m -> Set Symbol -> Sign f e -> Result (Morphism f e m)
generatedSign DefMorExt CASL_DLSign
forall e. DefMorExt e
emptyMorExt
         induced_from_morphism :: CASL_DL
-> EndoMap RawSymbol
-> DLSign
-> Result (Morphism DL_FORMULA CASL_DLSign (DefMorExt CASL_DLSign))
induced_from_morphism CASL_DL = DefMorExt CASL_DLSign
-> EndoMap RawSymbol
-> DLSign
-> Result (Morphism DL_FORMULA CASL_DLSign (DefMorExt CASL_DLSign))
forall e f m.
(Pretty e, Show f) =>
m -> EndoMap RawSymbol -> Sign f e -> Result (Morphism f e m)
inducedFromMorphism DefMorExt CASL_DLSign
forall e. DefMorExt e
emptyMorExt
         induced_from_to_morphism :: CASL_DL
-> EndoMap RawSymbol
-> ExtSign DLSign Symbol
-> ExtSign DLSign Symbol
-> Result (Morphism DL_FORMULA CASL_DLSign (DefMorExt CASL_DLSign))
induced_from_to_morphism CASL_DL =
             DefMorExt CASL_DLSign
-> (CASL_DLSign -> CASL_DLSign -> Bool)
-> (CASL_DLSign -> CASL_DLSign -> CASL_DLSign)
-> EndoMap RawSymbol
-> ExtSign DLSign Symbol
-> ExtSign DLSign Symbol
-> Result (Morphism DL_FORMULA CASL_DLSign (DefMorExt CASL_DLSign))
forall e f m.
(Eq e, Show f, Pretty e, Pretty m) =>
m
-> (e -> e -> Bool)
-> (e -> e -> e)
-> EndoMap RawSymbol
-> ExtSign (Sign f e) Symbol
-> ExtSign (Sign f e) Symbol
-> Result (Morphism f e m)
inducedFromToMorphism DefMorExt CASL_DLSign
forall e. DefMorExt e
emptyMorExt CASL_DLSign -> CASL_DLSign -> Bool
isSubCASL_DLSign CASL_DLSign -> CASL_DLSign -> CASL_DLSign
diffCASL_DLSign
         theory_to_taxonomy :: CASL_DL
-> TaxoGraphKind
-> MMiSSOntology
-> DLSign
-> [Named (FORMULA DL_FORMULA)]
-> Result MMiSSOntology
theory_to_taxonomy CASL_DL tgk :: TaxoGraphKind
tgk mo :: MMiSSOntology
mo =
             TaxoGraphKind
-> MMiSSOntology
-> DLSign
-> [Named (FORMULA DL_FORMULA)]
-> Result MMiSSOntology
forall f e.
TaxoGraphKind
-> MMiSSOntology
-> Sign f e
-> [Named (FORMULA f)]
-> Result MMiSSOntology
convTaxo TaxoGraphKind
tgk MMiSSOntology
mo (DLSign -> [Named (FORMULA DL_FORMULA)] -> Result MMiSSOntology)
-> (DLSign -> DLSign)
-> DLSign
-> [Named (FORMULA DL_FORMULA)]
-> Result MMiSSOntology
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DLSign -> DLSign
forall f e. Sign f e -> Sign f e
extendSortRelWithTopSort

-- | extend the sort relation with sort Thing for the taxonomy display
extendSortRelWithTopSort :: Sign f e -> Sign f e
extendSortRelWithTopSort :: Sign f e -> Sign f e
extendSortRelWithTopSort sig :: Sign f e
sig = Sign f e
sig {sortRel :: Rel Id
sortRel = Rel Id -> Rel Id
addThing (Rel Id -> Rel Id) -> Rel Id -> Rel Id
forall a b. (a -> b) -> a -> b
$ Sign f e -> Rel Id
forall f e. Sign f e -> Rel Id
sortRel Sign f e
sig}
    where addThing :: Rel Id -> Rel Id
addThing r :: Rel Id
r = Rel Id -> Rel Id -> Rel Id
forall a. Ord a => Rel a -> Rel a -> Rel a
Rel.union Rel Id
r (Set (Id, Id) -> Rel Id
forall a. Ord a => Set (a, a) -> Rel a
Rel.fromSet
                                    (Set (Id, Id) -> Rel Id) -> Set (Id, Id) -> Rel Id
forall a b. (a -> b) -> a -> b
$ (Id -> (Id, Id)) -> Set Id -> Set (Id, Id)
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (\ x :: Id
x -> (Id
x, Id
thing))
                                    (Set Id -> Set (Id, Id)) -> Set Id -> Set (Id, Id)
forall a b. (a -> b) -> a -> b
$ Sign f e -> Set Id
forall f e. Sign f e -> Set Id
sortSet Sign f e
sig)

instance Logic CASL_DL CASL_DL_SL
               DL_BASIC_SPEC DLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS
               DLSign
               DLMor
               Symbol RawSymbol ProofTree where
         stability :: CASL_DL -> Stability
stability _ = Stability
Experimental
         top_sublogic :: CASL_DL -> CASL_DL_SL
top_sublogic _ = CASL_DL_SL
SROIQ
         all_sublogics :: CASL_DL -> [CASL_DL_SL]
all_sublogics _ = [CASL_DL_SL
SROIQ]

instance MinSublogic CASL_DL_SL DLFORMULA where
    minSublogic :: FORMULA DL_FORMULA -> CASL_DL_SL
minSublogic _ = CASL_DL_SL
SROIQ

instance ProjectSublogic CASL_DL_SL DLMor where
    projectSublogic :: CASL_DL_SL
-> Morphism DL_FORMULA CASL_DLSign (DefMorExt CASL_DLSign)
-> Morphism DL_FORMULA CASL_DLSign (DefMorExt CASL_DLSign)
projectSublogic _ = Morphism DL_FORMULA CASL_DLSign (DefMorExt CASL_DLSign)
-> Morphism DL_FORMULA CASL_DLSign (DefMorExt CASL_DLSign)
forall a. a -> a
id

instance MinSublogic CASL_DL_SL DLMor where
    minSublogic :: Morphism DL_FORMULA CASL_DLSign (DefMorExt CASL_DLSign)
-> CASL_DL_SL
minSublogic _ = CASL_DL_SL
SROIQ

instance ProjectSublogic CASL_DL_SL DLSign where
    projectSublogic :: CASL_DL_SL -> DLSign -> DLSign
projectSublogic _ = DLSign -> DLSign
forall a. a -> a
id

instance MinSublogic CASL_DL_SL DLSign where
    minSublogic :: DLSign -> CASL_DL_SL
minSublogic _ = CASL_DL_SL
SROIQ

instance ProjectSublogicM CASL_DL_SL SYMB_MAP_ITEMS where
    projectSublogicM :: CASL_DL_SL -> SYMB_MAP_ITEMS -> Maybe SYMB_MAP_ITEMS
projectSublogicM _ = SYMB_MAP_ITEMS -> Maybe SYMB_MAP_ITEMS
forall a. a -> Maybe a
Just

instance ProjectSublogicM CASL_DL_SL SYMB_ITEMS where
    projectSublogicM :: CASL_DL_SL -> SYMB_ITEMS -> Maybe SYMB_ITEMS
projectSublogicM _ = SYMB_ITEMS -> Maybe SYMB_ITEMS
forall a. a -> Maybe a
Just

instance MinSublogic CASL_DL_SL SYMB_MAP_ITEMS where
    minSublogic :: SYMB_MAP_ITEMS -> CASL_DL_SL
minSublogic _ = CASL_DL_SL
SROIQ

instance MinSublogic CASL_DL_SL SYMB_ITEMS where
    minSublogic :: SYMB_ITEMS -> CASL_DL_SL
minSublogic _ = CASL_DL_SL
SROIQ

instance ProjectSublogic CASL_DL_SL DL_BASIC_SPEC where
    projectSublogic :: CASL_DL_SL -> DL_BASIC_SPEC -> DL_BASIC_SPEC
projectSublogic _ = DL_BASIC_SPEC -> DL_BASIC_SPEC
forall a. a -> a
id

instance MinSublogic CASL_DL_SL DL_BASIC_SPEC where
    minSublogic :: DL_BASIC_SPEC -> CASL_DL_SL
minSublogic _ = CASL_DL_SL
SROIQ

instance SublogicName CASL_DL_SL where
    sublogicName :: CASL_DL_SL -> String
sublogicName SROIQ = CASL_DL_SL -> String
forall a. Show a => a -> String
show CASL_DL_SL
SROIQ

instance SemiLatticeWithTop CASL_DL_SL where
    lub :: CASL_DL_SL -> CASL_DL_SL -> CASL_DL_SL
lub _ _ = CASL_DL_SL
SROIQ
    top :: CASL_DL_SL
top = CASL_DL_SL
SROIQ

instance ProjectSublogic CASL_DL_SL Symbol where
    projectSublogic :: CASL_DL_SL -> Symbol -> Symbol
projectSublogic _ = Symbol -> Symbol
forall a. a -> a
id

instance ProjectSublogicM CASL_DL_SL Symbol where
    projectSublogicM :: CASL_DL_SL -> Symbol -> Maybe Symbol
projectSublogicM _ = Symbol -> Maybe Symbol
forall a. a -> Maybe a
Just

instance MinSublogic CASL_DL_SL Symbol where
    minSublogic :: Symbol -> CASL_DL_SL
minSublogic _ = CASL_DL_SL
SROIQ