{-# LANGUAGE CPP, MultiParamTypeClasses, TypeSynonymInstances #-}
{-# OPTIONS -w #-}
{- |
Module      :  ./OWL2/Logic_OWL2.hs
Description :  instance of the class Logic for OWL2
Copyright   :  (c) Christian Maeder, DFKI GmbH 2011
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  Christian.Maeder@dfki.de
Stability   :  provisional
Portability :  non-portable

Here is the place where the class Logic is instantiated for OWL2.
-}

module OWL2.Logic_OWL2 where

import ATC.ProofTree ()
import OWL2.ATC_OWL2 ()

import Common.AS_Annotation as Anno
import Common.Consistency
import Common.DefaultMorphism
import Common.Doc
import Common.DocUtils
import Common.ProofTree
import Common.ProverTools
import Common.IRI

import Common.ExtSign
import Common.Result

import Data.Char (isAlpha)
import Data.Monoid
import Data.Maybe (fromJust)
import qualified Data.Map as Map
import qualified Data.Set as Set

import Logic.Logic

import OWL2.AS
--import OWL2.ATC_OWL2 ()
import OWL2.ColimSign
import OWL2.Conservativity
--import OWL2.MS2Ship
import qualified OWL2.PrintMS as PrMS (printOntologyDocument)
import qualified OWL2.PrintAS as PrAS (printOntologyDocument, printAxiom)
import OWL2.Pretty
import OWL2.Morphism
import qualified OWL2.ParseMS as PaMS (parseOntologyDocument)
import qualified OWL2.ParseAS as PaAS (parseOntologyDocument) 
import OWL2.ManchesterPrint (convertBasicTheory, convertBasicTheory')
import OWL2.Parse (symbItem, symbItems, symbMapItems) --temporary
import OWL2.ProfilesAndSublogics
import OWL2.ProveFact
import OWL2.ProvePellet
import OWL2.ProveHermit
import OWL2.Rename
import OWL2.Sign
import OWL2.StaticAnalysis
import OWL2.Symbols
import OWL2.Taxonomy
import OWL2.Theorem
-- import OWL2.ExtractModule
import ATerm.Conversion

data OWL2 = OWL2


instance Show OWL2 where
  show :: OWL2 -> String
show _ = "OWL"

instance Language OWL2 where
  description :: OWL2 -> String
description _ =
    "OWL -- Web Ontology Language http://www.w3.org/TR/owl2-overview/"

instance Category Sign OWLMorphism where
    ide :: Sign -> OWLMorphism
ide sig :: Sign
sig = Sign -> Sign -> OWLMorphism
inclOWLMorphism Sign
sig Sign
sig
    dom :: OWLMorphism -> Sign
dom = OWLMorphism -> Sign
osource
    cod :: OWLMorphism -> Sign
cod = OWLMorphism -> Sign
otarget
    legal_mor :: OWLMorphism -> Result ()
legal_mor = OWLMorphism -> Result ()
legalMor
    isInclusion :: OWLMorphism -> Bool
isInclusion = OWLMorphism -> Bool
isOWLInclusion
    composeMorphisms :: OWLMorphism -> OWLMorphism -> Result OWLMorphism
composeMorphisms = OWLMorphism -> OWLMorphism -> Result OWLMorphism
composeMor

instance Semigroup Ontology where
    (Ontology n :: Maybe OntologyIRI
n v :: Maybe OntologyIRI
v i1 :: DirectlyImportsDocuments
i1 a1 :: OntologyAnnotations
a1 ax1 :: [Axiom]
ax1) <> :: Ontology -> Ontology -> Ontology
<> (Ontology _ _ i2 :: DirectlyImportsDocuments
i2 a2 :: OntologyAnnotations
a2 ax2 :: [Axiom]
ax2) =
        Maybe OntologyIRI
-> Maybe OntologyIRI
-> DirectlyImportsDocuments
-> OntologyAnnotations
-> [Axiom]
-> Ontology
Ontology Maybe OntologyIRI
n Maybe OntologyIRI
v (DirectlyImportsDocuments
i1 DirectlyImportsDocuments
-> DirectlyImportsDocuments -> DirectlyImportsDocuments
forall a. [a] -> [a] -> [a]
++ DirectlyImportsDocuments
i2) (OntologyAnnotations
a1 OntologyAnnotations -> OntologyAnnotations -> OntologyAnnotations
forall a. [a] -> [a] -> [a]
++ OntologyAnnotations
a2) ([Axiom]
ax1 [Axiom] -> [Axiom] -> [Axiom]
forall a. [a] -> [a] -> [a]
++ [Axiom]
ax2)
instance Monoid Ontology where
    mempty :: Ontology
mempty = Maybe OntologyIRI
-> Maybe OntologyIRI
-> DirectlyImportsDocuments
-> OntologyAnnotations
-> [Axiom]
-> Ontology
Ontology Maybe OntologyIRI
forall a. Maybe a
Nothing Maybe OntologyIRI
forall a. Maybe a
Nothing [] [] []

instance Semigroup OntologyDocument where
    (OntologyDocument m :: OntologyMetadata
m p1 :: PrefixMap
p1 o1 :: Ontology
o1) <> :: OntologyDocument -> OntologyDocument -> OntologyDocument
<> (OntologyDocument _ p2 :: PrefixMap
p2 o2 :: Ontology
o2) =
      OntologyMetadata -> PrefixMap -> Ontology -> OntologyDocument
OntologyDocument OntologyMetadata
m (PrefixMap -> PrefixMap -> PrefixMap
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union PrefixMap
p1 PrefixMap
p2) (Ontology -> OntologyDocument) -> Ontology -> OntologyDocument
forall a b. (a -> b) -> a -> b
$ Ontology -> Ontology -> Ontology
forall a. Monoid a => a -> a -> a
mappend Ontology
o1 Ontology
o2
instance Monoid OntologyDocument where
    mempty :: OntologyDocument
mempty = OntologyMetadata -> PrefixMap -> Ontology -> OntologyDocument
OntologyDocument (OntologySyntaxType -> OntologyMetadata
OntologyMetadata OntologySyntaxType
AS) PrefixMap
forall a. Monoid a => a
mempty Ontology
forall a. Monoid a => a
mempty

instance Syntax OWL2 OntologyDocument Entity SymbItems SymbMapItems where
    parsersAndPrinters :: OWL2
-> Map
     String
     (PrefixMap -> AParser st OntologyDocument, OntologyDocument -> Doc)
parsersAndPrinters OWL2 = -- addSyntax "Ship" (parseOntologyDocument, ppShipOnt) 
      String
-> (PrefixMap -> AParser st OntologyDocument,
    OntologyDocument -> Doc)
-> Map
     String
     (PrefixMap -> AParser st OntologyDocument, OntologyDocument -> Doc)
-> Map
     String
     (PrefixMap -> AParser st OntologyDocument, OntologyDocument -> Doc)
forall b. String -> b -> Map String b -> Map String b
addSyntax "Manchester" (PrefixMap -> AParser st OntologyDocument
forall st. PrefixMap -> CharParser st OntologyDocument
PaMS.parseOntologyDocument, OntologyDocument -> Doc
PrMS.printOntologyDocument)
      (Map
   String
   (PrefixMap -> AParser st OntologyDocument, OntologyDocument -> Doc)
 -> Map
      String
      (PrefixMap -> AParser st OntologyDocument,
       OntologyDocument -> Doc))
-> Map
     String
     (PrefixMap -> AParser st OntologyDocument, OntologyDocument -> Doc)
-> Map
     String
     (PrefixMap -> AParser st OntologyDocument, OntologyDocument -> Doc)
forall a b. (a -> b) -> a -> b
$ String
-> (PrefixMap -> AParser st OntologyDocument,
    OntologyDocument -> Doc)
-> Map
     String
     (PrefixMap -> AParser st OntologyDocument, OntologyDocument -> Doc)
-> Map
     String
     (PrefixMap -> AParser st OntologyDocument, OntologyDocument -> Doc)
forall b. String -> b -> Map String b -> Map String b
addSyntax "Functional" (PrefixMap -> AParser st OntologyDocument
forall st. PrefixMap -> CharParser st OntologyDocument
PaAS.parseOntologyDocument, OntologyDocument -> Doc
PrAS.printOntologyDocument)
      (Map
   String
   (PrefixMap -> AParser st OntologyDocument, OntologyDocument -> Doc)
 -> Map
      String
      (PrefixMap -> AParser st OntologyDocument,
       OntologyDocument -> Doc))
-> Map
     String
     (PrefixMap -> AParser st OntologyDocument, OntologyDocument -> Doc)
-> Map
     String
     (PrefixMap -> AParser st OntologyDocument, OntologyDocument -> Doc)
forall a b. (a -> b) -> a -> b
$ (PrefixMap -> AParser st OntologyDocument, OntologyDocument -> Doc)
-> Map
     String
     (PrefixMap -> AParser st OntologyDocument, OntologyDocument -> Doc)
forall b. b -> Map String b
makeDefault (PrefixMap -> AParser st OntologyDocument
forall st. PrefixMap -> CharParser st OntologyDocument
PaMS.parseOntologyDocument, OntologyDocument -> Doc
PrMS.printOntologyDocument)
    parseSingleSymbItem :: OWL2 -> Maybe (PrefixMap -> AParser st SymbItems)
parseSingleSymbItem OWL2 = (PrefixMap -> AParser st SymbItems)
-> Maybe (PrefixMap -> AParser st SymbItems)
forall a. a -> Maybe a
Just ((PrefixMap -> AParser st SymbItems)
 -> Maybe (PrefixMap -> AParser st SymbItems))
-> (AParser st SymbItems -> PrefixMap -> AParser st SymbItems)
-> AParser st SymbItems
-> Maybe (PrefixMap -> AParser st SymbItems)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AParser st SymbItems -> PrefixMap -> AParser st SymbItems
forall a b. a -> b -> a
const (AParser st SymbItems -> Maybe (PrefixMap -> AParser st SymbItems))
-> AParser st SymbItems
-> Maybe (PrefixMap -> AParser st SymbItems)
forall a b. (a -> b) -> a -> b
$ AParser st SymbItems
forall st. GenParser Char st SymbItems
symbItem
    parse_symb_items :: OWL2 -> Maybe (PrefixMap -> AParser st SymbItems)
parse_symb_items OWL2 = (PrefixMap -> AParser st SymbItems)
-> Maybe (PrefixMap -> AParser st SymbItems)
forall a. a -> Maybe a
Just ((PrefixMap -> AParser st SymbItems)
 -> Maybe (PrefixMap -> AParser st SymbItems))
-> (AParser st SymbItems -> PrefixMap -> AParser st SymbItems)
-> AParser st SymbItems
-> Maybe (PrefixMap -> AParser st SymbItems)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AParser st SymbItems -> PrefixMap -> AParser st SymbItems
forall a b. a -> b -> a
const (AParser st SymbItems -> Maybe (PrefixMap -> AParser st SymbItems))
-> AParser st SymbItems
-> Maybe (PrefixMap -> AParser st SymbItems)
forall a b. (a -> b) -> a -> b
$ AParser st SymbItems
forall st. GenParser Char st SymbItems
symbItems
    parse_symb_map_items :: OWL2 -> Maybe (PrefixMap -> AParser st SymbMapItems)
parse_symb_map_items OWL2 = (PrefixMap -> AParser st SymbMapItems)
-> Maybe (PrefixMap -> AParser st SymbMapItems)
forall a. a -> Maybe a
Just ((PrefixMap -> AParser st SymbMapItems)
 -> Maybe (PrefixMap -> AParser st SymbMapItems))
-> (AParser st SymbMapItems
    -> PrefixMap -> AParser st SymbMapItems)
-> AParser st SymbMapItems
-> Maybe (PrefixMap -> AParser st SymbMapItems)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AParser st SymbMapItems -> PrefixMap -> AParser st SymbMapItems
forall a b. a -> b -> a
const (AParser st SymbMapItems
 -> Maybe (PrefixMap -> AParser st SymbMapItems))
-> AParser st SymbMapItems
-> Maybe (PrefixMap -> AParser st SymbMapItems)
forall a b. (a -> b) -> a -> b
$ AParser st SymbMapItems
forall st. GenParser Char st SymbMapItems
symbMapItems
    symb_items_name :: OWL2 -> SymbItems -> [String]
symb_items_name OWL2 = SymbItems -> [String]
symbItemsName


printOneNamed :: Anno.Named Axiom -> Doc
printOneNamed :: Named Axiom -> Doc
printOneNamed ns :: Named Axiom
ns = PrefixMap -> Axiom -> Doc
PrAS.printAxiom PrefixMap
forall a. Monoid a => a
mempty
  (Axiom -> Doc) -> Axiom -> Doc
forall a b. (a -> b) -> a -> b
$ (if Named Axiom -> Bool
forall s a. SenAttr s a -> Bool
Anno.isAxiom Named Axiom
ns then Axiom -> Axiom
rmImplied else Axiom -> Axiom
addImplied) (Axiom -> Axiom) -> Axiom -> Axiom
forall a b. (a -> b) -> a -> b
$ Named Axiom -> Axiom
forall s a. SenAttr s a -> s
Anno.sentence Named Axiom
ns

instance Sentences OWL2 Axiom Sign OWLMorphism Entity where
    map_sen :: OWL2 -> OWLMorphism -> Axiom -> Result Axiom
map_sen OWL2 = OWLMorphism -> Axiom -> Result Axiom
mapSen
    print_named :: OWL2 -> Named Axiom -> Doc
print_named OWL2 = Named Axiom -> Doc
printOneNamed
    sym_of :: OWL2 -> Sign -> [Set Entity]
sym_of OWL2 = Set Entity -> [Set Entity]
forall a. a -> [a]
singletonList (Set Entity -> [Set Entity])
-> (Sign -> Set Entity) -> Sign -> [Set Entity]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sign -> Set Entity
symOf
    symmap_of :: OWL2 -> OWLMorphism -> EndoMap Entity
symmap_of OWL2 = OWLMorphism -> EndoMap Entity
symMapOf
    sym_name :: OWL2 -> Entity -> Id
sym_name OWL2 = Entity -> Id
entityToId
    sym_label :: OWL2 -> Entity -> Maybe String
sym_label OWL2 = Entity -> Maybe String
label
    fullSymName :: OWL2 -> Entity -> String
fullSymName OWL2 s :: Entity
s = let
      i :: OntologyIRI
i = Entity -> OntologyIRI
cutIRI Entity
s
      x :: String
x = OntologyIRI -> String
showIRI OntologyIRI
i --expandedIRI i
      in if String -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
x then OntologyIRI -> String
getPredefName OntologyIRI
i else String
x
    symKind :: OWL2 -> Entity -> String
symKind OWL2 = (Char -> Bool) -> ShowS
forall a. (a -> Bool) -> [a] -> [a]
takeWhile Char -> Bool
isAlpha ShowS -> (Entity -> String) -> Entity -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. EntityType -> String
showEntityType (EntityType -> String)
-> (Entity -> EntityType) -> Entity -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Entity -> EntityType
entityKind
    symsOfSen :: OWL2 -> Sign -> Axiom -> [Entity]
symsOfSen OWL2 _ = Set Entity -> [Entity]
forall a. Set a -> [a]
Set.toList (Set Entity -> [Entity])
-> (Axiom -> Set Entity) -> Axiom -> [Entity]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Axiom -> Set Entity
symsOfAxiom
    pair_symbols :: OWL2 -> Entity -> Entity -> Result Entity
pair_symbols OWL2 = Entity -> Entity -> Result Entity
pairSymbols

inducedFromToMor :: Map.Map RawSymb RawSymb -> 
                    ExtSign Sign Entity -> 
                    ExtSign Sign Entity -> 
                    Result OWLMorphism
inducedFromToMor :: Map RawSymb RawSymb
-> ExtSign Sign Entity -> ExtSign Sign Entity -> Result OWLMorphism
inducedFromToMor rm :: Map RawSymb RawSymb
rm s :: ExtSign Sign Entity
s@(ExtSign ssig :: Sign
ssig _) t :: ExtSign Sign Entity
t@(ExtSign tsig :: Sign
tsig _) = 
 case Map RawSymb RawSymb -> [(RawSymb, RawSymb)]
forall k a. Map k a -> [(k, a)]
Map.toList Map RawSymb RawSymb
rm of
   [] -> do 
     let 
       mkImplMap :: (Sign -> Set OntologyIRI) -> EntityType -> Map RawSymb RawSymb
mkImplMap f :: Sign -> Set OntologyIRI
f k :: EntityType
k = 
         case Set OntologyIRI -> DirectlyImportsDocuments
forall a. Set a -> [a]
Set.toList (Sign -> Set OntologyIRI
f Sign
tsig) of 
           [x :: OntologyIRI
x] -> 
              let aEntity :: Entity
aEntity = Maybe String -> EntityType -> OntologyIRI -> Entity
Entity Maybe String
forall a. Maybe a
Nothing EntityType
k OntologyIRI
x
              in [(RawSymb, RawSymb)] -> Map RawSymb RawSymb
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(RawSymb, RawSymb)] -> Map RawSymb RawSymb)
-> [(RawSymb, RawSymb)] -> Map RawSymb RawSymb
forall a b. (a -> b) -> a -> b
$ 
                    (OntologyIRI -> (RawSymb, RawSymb))
-> DirectlyImportsDocuments -> [(RawSymb, RawSymb)]
forall a b. (a -> b) -> [a] -> [b]
map (\y :: OntologyIRI
y -> (Entity -> RawSymb
ASymbol (Entity -> RawSymb) -> Entity -> RawSymb
forall a b. (a -> b) -> a -> b
$ Maybe String -> EntityType -> OntologyIRI -> Entity
Entity Maybe String
forall a. Maybe a
Nothing EntityType
k OntologyIRI
y, 
                               Entity -> RawSymb
ASymbol (Entity -> RawSymb) -> Entity -> RawSymb
forall a b. (a -> b) -> a -> b
$ Entity
aEntity)) (DirectlyImportsDocuments -> [(RawSymb, RawSymb)])
-> DirectlyImportsDocuments -> [(RawSymb, RawSymb)]
forall a b. (a -> b) -> a -> b
$ 
                    Set OntologyIRI -> DirectlyImportsDocuments
forall a. Set a -> [a]
Set.toList (Set OntologyIRI -> DirectlyImportsDocuments)
-> Set OntologyIRI -> DirectlyImportsDocuments
forall a b. (a -> b) -> a -> b
$ Sign -> Set OntologyIRI
f Sign
ssig
           _ -> Map RawSymb RawSymb
forall k a. Map k a
Map.empty 
       rm' :: Map RawSymb RawSymb
rm' = [Map RawSymb RawSymb] -> Map RawSymb RawSymb
forall (f :: * -> *) k a.
(Foldable f, Ord k) =>
f (Map k a) -> Map k a
Map.unions
                   [(Sign -> Set OntologyIRI) -> EntityType -> Map RawSymb RawSymb
mkImplMap Sign -> Set OntologyIRI
concepts EntityType
Class,
                    (Sign -> Set OntologyIRI) -> EntityType -> Map RawSymb RawSymb
mkImplMap Sign -> Set OntologyIRI
objectProperties EntityType
ObjectProperty,
                    (Sign -> Set OntologyIRI) -> EntityType -> Map RawSymb RawSymb
mkImplMap Sign -> Set OntologyIRI
dataProperties EntityType
DataProperty, 
                    (Sign -> Set OntologyIRI) -> EntityType -> Map RawSymb RawSymb
mkImplMap Sign -> Set OntologyIRI
individuals EntityType
NamedIndividual]
      in Map RawSymb RawSymb
-> ExtSign Sign Entity -> ExtSign Sign Entity -> Result OWLMorphism
inducedFromToMorphismAux Map RawSymb RawSymb
rm' ExtSign Sign Entity
s ExtSign Sign Entity
t 
   _ ->  Map RawSymb RawSymb
-> ExtSign Sign Entity -> ExtSign Sign Entity -> Result OWLMorphism
inducedFromToMorphismAux Map RawSymb RawSymb
rm  ExtSign Sign Entity
s ExtSign Sign Entity
t

inducedFromToMorphismAux :: Map.Map RawSymb RawSymb -> 
                    ExtSign Sign Entity -> 
                    ExtSign Sign Entity -> 
                    Result OWLMorphism
inducedFromToMorphismAux :: Map RawSymb RawSymb
-> ExtSign Sign Entity -> ExtSign Sign Entity -> Result OWLMorphism
inducedFromToMorphismAux rm :: Map RawSymb RawSymb
rm s :: ExtSign Sign Entity
s@(ExtSign ssig :: Sign
ssig _) t :: ExtSign Sign Entity
t@(ExtSign tsig :: Sign
tsig _) = do
    OWLMorphism
mor <- Map RawSymb RawSymb -> Sign -> Result OWLMorphism
inducedFromMor Map RawSymb RawSymb
rm Sign
ssig
    let csig :: Sign
csig = OWLMorphism -> Sign
forall object morphism.
Category object morphism =>
morphism -> object
cod OWLMorphism
mor
    OWLMorphism
incl <- OWL2 -> Sign -> Sign -> Result OWLMorphism
forall lid basic_spec sentence symb_items symb_map_items sign
       morphism symbol raw_symbol.
StaticAnalysis
  lid
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol =>
lid -> sign -> sign -> Result morphism
inclusion OWL2
OWL2 Sign
csig Sign
tsig              
    OWLMorphism -> OWLMorphism -> Result OWLMorphism
forall object morphism.
Category object morphism =>
morphism -> morphism -> Result morphism
composeMorphisms OWLMorphism
mor OWLMorphism
incl

instance StaticAnalysis OWL2 OntologyDocument Axiom
               SymbItems SymbMapItems
               Sign
               OWLMorphism
               Entity RawSymb where
      basic_analysis :: OWL2
-> Maybe
     ((OntologyDocument, Sign, GlobalAnnos)
      -> Result (OntologyDocument, ExtSign Sign Entity, [Named Axiom]))
basic_analysis OWL2 = ((OntologyDocument, Sign, GlobalAnnos)
 -> Result (OntologyDocument, ExtSign Sign Entity, [Named Axiom]))
-> Maybe
     ((OntologyDocument, Sign, GlobalAnnos)
      -> Result (OntologyDocument, ExtSign Sign Entity, [Named Axiom]))
forall a. a -> Maybe a
Just (OntologyDocument, Sign, GlobalAnnos)
-> Result (OntologyDocument, ExtSign Sign Entity, [Named Axiom])
basicOWL2Analysis
      stat_symb_items :: OWL2 -> Sign -> [SymbItems] -> Result [RawSymb]
stat_symb_items OWL2 s :: Sign
s = [RawSymb] -> Result [RawSymb]
forall (m :: * -> *) a. Monad m => a -> m a
return ([RawSymb] -> Result [RawSymb])
-> ([SymbItems] -> [RawSymb]) -> [SymbItems] -> Result [RawSymb]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sign -> [SymbItems] -> [RawSymb]
statSymbItems Sign
s
      stat_symb_map_items :: OWL2
-> Sign
-> Maybe Sign
-> [SymbMapItems]
-> Result (Map RawSymb RawSymb)
stat_symb_map_items OWL2 = Sign
-> Maybe Sign -> [SymbMapItems] -> Result (Map RawSymb RawSymb)
statSymbMapItems
      convertTheory :: OWL2 -> Maybe ((Sign, [Named Axiom]) -> OntologyDocument)
convertTheory OWL2 = ((Sign, [Named Axiom]) -> OntologyDocument)
-> Maybe ((Sign, [Named Axiom]) -> OntologyDocument)
forall a. a -> Maybe a
Just (Sign, [Named Axiom]) -> OntologyDocument
convertBasicTheory
      empty_signature :: OWL2 -> Sign
empty_signature OWL2 = Sign
emptySign
      signature_union :: OWL2 -> Sign -> Sign -> Result Sign
signature_union OWL2 = Sign -> Sign -> Result Sign
uniteSign
      intersection :: OWL2 -> Sign -> Sign -> Result Sign
intersection OWL2 = Sign -> Sign -> Result Sign
intersectSign
      morphism_union :: OWL2 -> OWLMorphism -> OWLMorphism -> Result OWLMorphism
morphism_union OWL2  = OWLMorphism -> OWLMorphism -> Result OWLMorphism
morphismUnion
      signatureDiff :: OWL2 -> Sign -> Sign -> Result Sign
signatureDiff OWL2 s :: Sign
s = Sign -> Result Sign
forall (m :: * -> *) a. Monad m => a -> m a
return (Sign -> Result Sign) -> (Sign -> Sign) -> Sign -> Result Sign
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sign -> Sign -> Sign
diffSig Sign
s
      final_union :: OWL2 -> Sign -> Sign -> Result Sign
final_union OWL2 = OWL2 -> Sign -> Sign -> Result Sign
forall lid basic_spec sentence symb_items symb_map_items sign
       morphism symbol raw_symbol.
StaticAnalysis
  lid
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol =>
lid -> sign -> sign -> Result sign
signature_union OWL2
OWL2
      is_subsig :: OWL2 -> Sign -> Sign -> Bool
is_subsig OWL2 = Sign -> Sign -> Bool
isSubSign
      subsig_inclusion :: OWL2 -> Sign -> Sign -> Result OWLMorphism
subsig_inclusion OWL2 s :: Sign
s = OWLMorphism -> Result OWLMorphism
forall (m :: * -> *) a. Monad m => a -> m a
return (OWLMorphism -> Result OWLMorphism)
-> (Sign -> OWLMorphism) -> Sign -> Result OWLMorphism
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sign -> Sign -> OWLMorphism
inclOWLMorphism Sign
s
      matches :: OWL2 -> Entity -> RawSymb -> Bool
matches OWL2 = Entity -> RawSymb -> Bool
matchesSym
      symbol_to_raw :: OWL2 -> Entity -> RawSymb
symbol_to_raw OWL2 = Entity -> RawSymb
ASymbol
      id_to_raw :: OWL2 -> Id -> RawSymb
id_to_raw OWL2 = Id -> RawSymb
idToRaw
      add_symb_to_sign :: OWL2 -> Sign -> Entity -> Result Sign
add_symb_to_sign OWL2 = Sign -> Entity -> Result Sign
addSymbToSign
      induced_from_morphism :: OWL2 -> Map RawSymb RawSymb -> Sign -> Result OWLMorphism
induced_from_morphism OWL2 = Map RawSymb RawSymb -> Sign -> Result OWLMorphism
inducedFromMor
      induced_from_to_morphism :: OWL2
-> Map RawSymb RawSymb
-> ExtSign Sign Entity
-> ExtSign Sign Entity
-> Result OWLMorphism
induced_from_to_morphism OWL2 = Map RawSymb RawSymb
-> ExtSign Sign Entity -> ExtSign Sign Entity -> Result OWLMorphism
inducedFromToMor
      cogenerated_sign :: OWL2 -> Set Entity -> Sign -> Result OWLMorphism
cogenerated_sign OWL2 = Set Entity -> Sign -> Result OWLMorphism
cogeneratedSign
      generated_sign :: OWL2 -> Set Entity -> Sign -> Result OWLMorphism
generated_sign OWL2 = Set Entity -> Sign -> Result OWLMorphism
generatedSign
      signature_colimit :: OWL2
-> Gr Sign (Int, OWLMorphism) -> Result (Sign, Map Int OWLMorphism)
signature_colimit OWL2 = (Sign, Map Int OWLMorphism) -> Result (Sign, Map Int OWLMorphism)
forall (m :: * -> *) a. Monad m => a -> m a
return ((Sign, Map Int OWLMorphism) -> Result (Sign, Map Int OWLMorphism))
-> (Gr Sign (Int, OWLMorphism) -> (Sign, Map Int OWLMorphism))
-> Gr Sign (Int, OWLMorphism)
-> Result (Sign, Map Int OWLMorphism)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Gr Sign (Int, OWLMorphism) -> (Sign, Map Int OWLMorphism)
signColimit
      corresp2th :: OWL2
-> String
-> Bool
-> Sign
-> Sign
-> [SymbItems]
-> [SymbItems]
-> EndoMap Entity
-> EndoMap Entity
-> REL_REF
-> Result
     (Sign, [Named Axiom], Sign, Sign, EndoMap Entity, EndoMap Entity)
corresp2th OWL2 = String
-> Bool
-> Sign
-> Sign
-> [SymbItems]
-> [SymbItems]
-> EndoMap Entity
-> EndoMap Entity
-> REL_REF
-> Result
     (Sign, [Named Axiom], Sign, Sign, EndoMap Entity, EndoMap Entity)
corr2theo
      equiv2cospan :: OWL2
-> Sign
-> Sign
-> [SymbItems]
-> [SymbItems]
-> Result (Sign, Sign, Sign, EndoMap Entity, EndoMap Entity)
equiv2cospan OWL2 = Sign
-> Sign
-> [SymbItems]
-> [SymbItems]
-> Result (Sign, Sign, Sign, EndoMap Entity, EndoMap Entity)
addEquiv
    --   extract_module OWL2 = extractModule
#ifdef UNI_PACKAGE
      theory_to_taxonomy :: OWL2
-> TaxoGraphKind
-> MMiSSOntology
-> Sign
-> [Named Axiom]
-> Result MMiSSOntology
theory_to_taxonomy OWL2 = TaxoGraphKind
-> MMiSSOntology -> Sign -> [Named Axiom] -> Result MMiSSOntology
onto2Tax
#endif
instance Logic OWL2 ProfSub OntologyDocument Axiom SymbItems SymbMapItems
               Sign
               OWLMorphism Entity RawSymb ProofTree where
         empty_proof_tree :: OWL2 -> ProofTree
empty_proof_tree OWL2 = ProofTree
emptyProofTree
         -- just a selection of sublogics
         all_sublogics :: OWL2 -> [ProfSub]
all_sublogics OWL2 = ProfSub
bottomS ProfSub -> [ProfSub] -> [ProfSub]
forall a. a -> [a] -> [a]
: [[ProfSub]] -> [ProfSub]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[ProfSub]]
allProfSubs [ProfSub] -> [ProfSub] -> [ProfSub]
forall a. [a] -> [a] -> [a]
++ [ProfSub
topS]
         bottomSublogic :: OWL2 -> Maybe ProfSub
bottomSublogic OWL2 = ProfSub -> Maybe ProfSub
forall a. a -> Maybe a
Just ProfSub
bottomS
         sublogicDimensions :: OWL2 -> [[ProfSub]]
sublogicDimensions OWL2 = [[ProfSub]]
allProfSubs
         parseSublogic :: OWL2 -> String -> Maybe ProfSub
parseSublogic OWL2 _ = ProfSub -> Maybe ProfSub
forall a. a -> Maybe a
Just ProfSub
topS -- ignore sublogics
         provers :: OWL2 -> [Prover Sign Axiom OWLMorphism ProfSub ProofTree]
provers OWL2 = [Prover Sign Axiom OWLMorphism ProfSub ProofTree
pelletProver, Prover Sign Axiom OWLMorphism ProfSub ProofTree
factProver, Prover Sign Axiom OWLMorphism ProfSub ProofTree
hermitProver]
         default_prover :: OWL2 -> String
default_prover OWL2 = "Fact"
         cons_checkers :: OWL2 -> [ConsChecker Sign Axiom ProfSub OWLMorphism ProofTree]
cons_checkers OWL2 = [ConsChecker Sign Axiom ProfSub OWLMorphism ProofTree
pelletConsChecker, ConsChecker Sign Axiom ProfSub OWLMorphism ProofTree
factConsChecker, ConsChecker Sign Axiom ProfSub OWLMorphism ProofTree
hermitConsChecker]
         conservativityCheck :: OWL2 -> [ConservativityChecker Sign Axiom OWLMorphism]
conservativityCheck OWL2 = (String -> ConservativityChecker Sign Axiom OWLMorphism)
-> [String] -> [ConservativityChecker Sign Axiom OWLMorphism]
forall a b. (a -> b) -> [a] -> [b]
map
           (\ ct :: String
ct -> String
-> IO (Maybe String)
-> ((Sign, [Named Axiom])
    -> OWLMorphism
    -> [Named Axiom]
    -> IO (Result (Conservativity, [Axiom])))
-> ConservativityChecker Sign Axiom OWLMorphism
forall sign sentence morphism.
String
-> IO (Maybe String)
-> ((sign, [Named sentence])
    -> morphism
    -> [Named sentence]
    -> IO (Result (Conservativity, [sentence])))
-> ConservativityChecker sign sentence morphism
ConservativityChecker ("Locality_" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
ct)
                    (String -> IO (Maybe String)
checkOWLjar String
localityJar) (((Sign, [Named Axiom])
  -> OWLMorphism
  -> [Named Axiom]
  -> IO (Result (Conservativity, [Axiom])))
 -> ConservativityChecker Sign Axiom OWLMorphism)
-> ((Sign, [Named Axiom])
    -> OWLMorphism
    -> [Named Axiom]
    -> IO (Result (Conservativity, [Axiom])))
-> ConservativityChecker Sign Axiom OWLMorphism
forall a b. (a -> b) -> a -> b
$ String
-> (Sign, [Named Axiom])
-> OWLMorphism
-> [Named Axiom]
-> IO (Result (Conservativity, [Axiom]))
conserCheck String
ct)
           ["BOTTOM_BOTTOM", "TOP_BOTTOM", "TOP_TOP"]
         stability :: OWL2 -> Stability
stability OWL2 = Stability
Stable
         sublogicOfTheo :: OWL2 -> (Sign, [Axiom]) -> ProfSub
sublogicOfTheo OWL2 = OntologyDocument -> ProfSub
profilesAndSublogic (OntologyDocument -> ProfSub)
-> ((Sign, [Axiom]) -> OntologyDocument)
-> (Sign, [Axiom])
-> ProfSub
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Sign, [Axiom]) -> OntologyDocument
convertBasicTheory'

instance SemiLatticeWithTop ProfSub where
    lub :: ProfSub -> ProfSub -> ProfSub
lub = ProfSub -> ProfSub -> ProfSub
maxS
    top :: ProfSub
top = ProfSub
topS

instance SublogicName ProfSub where
    sublogicName :: ProfSub -> String
sublogicName = ProfSub -> String
nameS

instance MinSublogic ProfSub Axiom where
    minSublogic :: Axiom -> ProfSub
minSublogic = Axiom -> ProfSub
psAxiom

instance MinSublogic ProfSub OWLMorphism where
    minSublogic :: OWLMorphism -> ProfSub
minSublogic = OWLMorphism -> ProfSub
sMorph

instance ProjectSublogic ProfSub OWLMorphism where
    projectSublogic :: ProfSub -> OWLMorphism -> OWLMorphism
projectSublogic = ProfSub -> OWLMorphism -> OWLMorphism
prMorph

instance MinSublogic ProfSub Sign where
    minSublogic :: Sign -> ProfSub
minSublogic = Sign -> ProfSub
sSig

instance ProjectSublogic ProfSub Sign where
    projectSublogic :: ProfSub -> Sign -> Sign
projectSublogic = ProfSub -> Sign -> Sign
prSign

instance MinSublogic ProfSub SymbItems where
    minSublogic :: SymbItems -> ProfSub
minSublogic = ProfSub -> SymbItems -> ProfSub
forall a b. a -> b -> a
const ProfSub
topS

instance MinSublogic ProfSub SymbMapItems where
    minSublogic :: SymbMapItems -> ProfSub
minSublogic = ProfSub -> SymbMapItems -> ProfSub
forall a b. a -> b -> a
const ProfSub
topS

instance MinSublogic ProfSub Entity where
    minSublogic :: Entity -> ProfSub
minSublogic = ProfSub -> Entity -> ProfSub
forall a b. a -> b -> a
const ProfSub
topS

instance MinSublogic ProfSub OntologyDocument where
    minSublogic :: OntologyDocument -> ProfSub
minSublogic = OntologyDocument -> ProfSub
profilesAndSublogic

instance ProjectSublogicM ProfSub SymbItems where
    projectSublogicM :: ProfSub -> SymbItems -> Maybe SymbItems
projectSublogicM = (SymbItems -> Maybe SymbItems)
-> ProfSub -> SymbItems -> Maybe SymbItems
forall a b. a -> b -> a
const SymbItems -> Maybe SymbItems
forall a. a -> Maybe a
Just

instance ProjectSublogicM ProfSub SymbMapItems where
    projectSublogicM :: ProfSub -> SymbMapItems -> Maybe SymbMapItems
projectSublogicM = (SymbMapItems -> Maybe SymbMapItems)
-> ProfSub -> SymbMapItems -> Maybe SymbMapItems
forall a b. a -> b -> a
const SymbMapItems -> Maybe SymbMapItems
forall a. a -> Maybe a
Just

instance ProjectSublogicM ProfSub Entity where
    projectSublogicM :: ProfSub -> Entity -> Maybe Entity
projectSublogicM = (Entity -> Maybe Entity) -> ProfSub -> Entity -> Maybe Entity
forall a b. a -> b -> a
const Entity -> Maybe Entity
forall a. a -> Maybe a
Just

instance ProjectSublogic ProfSub OntologyDocument where
    projectSublogic :: ProfSub -> OntologyDocument -> OntologyDocument
projectSublogic = ProfSub -> OntologyDocument -> OntologyDocument
prOntDoc