{- |
Module      :  ./OWL2/CreateOWL.hs
Description :  translate theories to OWL2
Copyright   :  (c) C. Maeder, DFKI GmbH 2012
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  Christian.Maeder@dfki.de
Stability   :  provisional
Portability :  non-portable (via Logic.Logic)
-}


module OWL2.CreateOWL where

import Common.Result
import Common.AS_Annotation
import Logic.Coerce
import Logic.Comorphism

import Static.GTheory
import Logic.Prover

import Common.ExtSign

import OWL2.Sign
import qualified OWL2.AS as AS
import OWL2.Logic_OWL2
import OWL2.CASL2OWL
import OWL2.DMU2OWL2
import OWL2.Propositional2OWL2

import CASL.Logic_CASL
import ExtModal.Logic_ExtModal
import Comorphisms.ExtModal2OWL

import DMU.Logic_DMU
import Propositional.Logic_Propositional

createOWLTheory :: G_theory -> Result (Sign, [Named AS.Axiom])
createOWLTheory :: G_theory -> Result (Sign, [Named Axiom])
createOWLTheory (G_theory lid :: lid
lid _ (ExtSign sign0 :: sign
sign0 _) _ sens0 :: ThSens sentence (AnyComorphism, BasicProof)
sens0 _) = do
    let th :: (sign, [Named sentence])
th = (sign
sign0, ThSens sentence (AnyComorphism, BasicProof) -> [Named sentence]
forall a b. ThSens a b -> [Named a]
toNamedList ThSens sentence (AnyComorphism, BasicProof)
sens0)
        r1 :: Result (CASLSign, [Named CASLFORMULA])
r1 = lid
-> CASL
-> String
-> (sign, [Named sentence])
-> Result (CASLSign, [Named CASLFORMULA])
forall lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2 (m :: * -> *).
(Logic
   lid1
   sublogics1
   basic_spec1
   sentence1
   symb_items1
   symb_map_items1
   sign1
   morphism1
   symbol1
   raw_symbol1
   proof_tree1,
 Logic
   lid2
   sublogics2
   basic_spec2
   sentence2
   symb_items2
   symb_map_items2
   sign2
   morphism2
   symbol2
   raw_symbol2
   proof_tree2,
 MonadFail m) =>
lid1
-> lid2
-> String
-> (sign1, [Named sentence1])
-> m (sign2, [Named sentence2])
coerceBasicTheory lid
lid CASL
CASL "" (sign, [Named sentence])
th
        r1' :: Result (Sign, [Named Axiom])
r1' = Result (CASLSign, [Named CASLFORMULA])
r1 Result (CASLSign, [Named CASLFORMULA])
-> ((CASLSign, [Named CASLFORMULA])
    -> Result (Sign, [Named Axiom]))
-> Result (Sign, [Named Axiom])
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= CASL2OWL
-> (CASLSign, [Named CASLFORMULA]) -> Result (Sign, [Named Axiom])
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid
-> (sign1, [Named sentence1]) -> Result (sign2, [Named sentence2])
wrapMapTheory CASL2OWL
CASL2OWL
        r2 :: Result (Text, [Named ()])
r2 = lid
-> DMU
-> String
-> (sign, [Named sentence])
-> Result (Text, [Named ()])
forall lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2 (m :: * -> *).
(Logic
   lid1
   sublogics1
   basic_spec1
   sentence1
   symb_items1
   symb_map_items1
   sign1
   morphism1
   symbol1
   raw_symbol1
   proof_tree1,
 Logic
   lid2
   sublogics2
   basic_spec2
   sentence2
   symb_items2
   symb_map_items2
   sign2
   morphism2
   symbol2
   raw_symbol2
   proof_tree2,
 MonadFail m) =>
lid1
-> lid2
-> String
-> (sign1, [Named sentence1])
-> m (sign2, [Named sentence2])
coerceBasicTheory lid
lid DMU
DMU "" (sign, [Named sentence])
th
        r2' :: Result (Sign, [Named Axiom])
r2' = Result (Text, [Named ()])
r2 Result (Text, [Named ()])
-> ((Text, [Named ()]) -> Result (Sign, [Named Axiom]))
-> Result (Sign, [Named Axiom])
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= DMU2OWL2 -> (Text, [Named ()]) -> Result (Sign, [Named Axiom])
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid
-> (sign1, [Named sentence1]) -> Result (sign2, [Named sentence2])
wrapMapTheory DMU2OWL2
DMU2OWL2
        r3 :: Result (Sign, [Named FORMULA])
r3 = lid
-> Propositional
-> String
-> (sign, [Named sentence])
-> Result (Sign, [Named FORMULA])
forall lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2 (m :: * -> *).
(Logic
   lid1
   sublogics1
   basic_spec1
   sentence1
   symb_items1
   symb_map_items1
   sign1
   morphism1
   symbol1
   raw_symbol1
   proof_tree1,
 Logic
   lid2
   sublogics2
   basic_spec2
   sentence2
   symb_items2
   symb_map_items2
   sign2
   morphism2
   symbol2
   raw_symbol2
   proof_tree2,
 MonadFail m) =>
lid1
-> lid2
-> String
-> (sign1, [Named sentence1])
-> m (sign2, [Named sentence2])
coerceBasicTheory lid
lid Propositional
Propositional "" (sign, [Named sentence])
th
        r3' :: Result (Sign, [Named Axiom])
r3' = Result (Sign, [Named FORMULA])
r3 Result (Sign, [Named FORMULA])
-> ((Sign, [Named FORMULA]) -> Result (Sign, [Named Axiom]))
-> Result (Sign, [Named Axiom])
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Propositional2OWL2
-> (Sign, [Named FORMULA]) -> Result (Sign, [Named Axiom])
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid
-> (sign1, [Named sentence1]) -> Result (sign2, [Named sentence2])
wrapMapTheory Propositional2OWL2
Propositional2OWL2
        r4 :: Result (ExtModalSign, [Named ExtModalFORMULA])
r4 = lid
-> ExtModal
-> String
-> (sign, [Named sentence])
-> Result (ExtModalSign, [Named ExtModalFORMULA])
forall lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2 (m :: * -> *).
(Logic
   lid1
   sublogics1
   basic_spec1
   sentence1
   symb_items1
   symb_map_items1
   sign1
   morphism1
   symbol1
   raw_symbol1
   proof_tree1,
 Logic
   lid2
   sublogics2
   basic_spec2
   sentence2
   symb_items2
   symb_map_items2
   sign2
   morphism2
   symbol2
   raw_symbol2
   proof_tree2,
 MonadFail m) =>
lid1
-> lid2
-> String
-> (sign1, [Named sentence1])
-> m (sign2, [Named sentence2])
coerceBasicTheory lid
lid ExtModal
ExtModal "" (sign, [Named sentence])
th
        r4' :: Result (Sign, [Named Axiom])
r4' = Result (ExtModalSign, [Named ExtModalFORMULA])
r4 Result (ExtModalSign, [Named ExtModalFORMULA])
-> ((ExtModalSign, [Named ExtModalFORMULA])
    -> Result (Sign, [Named Axiom]))
-> Result (Sign, [Named Axiom])
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= ExtModal2OWL
-> (ExtModalSign, [Named ExtModalFORMULA])
-> Result (Sign, [Named Axiom])
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid
-> (sign1, [Named sentence1]) -> Result (sign2, [Named sentence2])
wrapMapTheory ExtModal2OWL
ExtModal2OWL
        r5 :: Result (Sign, [Named Axiom])
r5 = lid
-> OWL2
-> String
-> (sign, [Named sentence])
-> Result (Sign, [Named Axiom])
forall lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2 (m :: * -> *).
(Logic
   lid1
   sublogics1
   basic_spec1
   sentence1
   symb_items1
   symb_map_items1
   sign1
   morphism1
   symbol1
   raw_symbol1
   proof_tree1,
 Logic
   lid2
   sublogics2
   basic_spec2
   sentence2
   symb_items2
   symb_map_items2
   sign2
   morphism2
   symbol2
   raw_symbol2
   proof_tree2,
 MonadFail m) =>
lid1
-> lid2
-> String
-> (sign1, [Named sentence1])
-> m (sign2, [Named sentence2])
coerceBasicTheory lid
lid OWL2
OWL2 "" (sign, [Named sentence])
th
        r6 :: Result (Sign, [Named Axiom])
r6 = case Result (CASLSign, [Named CASLFORMULA])
-> Maybe (CASLSign, [Named CASLFORMULA])
forall a. Result a -> Maybe a
maybeResult Result (CASLSign, [Named CASLFORMULA])
r1 of
               Nothing -> case Result (Text, [Named ()]) -> Maybe (Text, [Named ()])
forall a. Result a -> Maybe a
maybeResult Result (Text, [Named ()])
r2 of
                 Nothing -> case Result (Sign, [Named FORMULA]) -> Maybe (Sign, [Named FORMULA])
forall a. Result a -> Maybe a
maybeResult Result (Sign, [Named FORMULA])
r3 of
                   Nothing -> case Result (ExtModalSign, [Named ExtModalFORMULA])
-> Maybe (ExtModalSign, [Named ExtModalFORMULA])
forall a. Result a -> Maybe a
maybeResult Result (ExtModalSign, [Named ExtModalFORMULA])
r4 of
                     Nothing -> Result (Sign, [Named Axiom])
r5
                     _ -> Result (Sign, [Named Axiom])
r4'
                   _ -> Result (Sign, [Named Axiom])
r3'
                 _ -> Result (Sign, [Named Axiom])
r2'
               _ -> Result (Sign, [Named Axiom])
r1'

    (sign :: Sign
sign, sens :: [Named Axiom]
sens) <- Result (Sign, [Named Axiom])
r6
    (Sign, [Named Axiom]) -> Result (Sign, [Named Axiom])
forall (m :: * -> *) a. Monad m => a -> m a
return (Sign
sign, ThSens Axiom Any -> [Named Axiom]
forall a b. ThSens a b -> [Named a]
toNamedList (ThSens Axiom Any -> [Named Axiom])
-> ThSens Axiom Any -> [Named Axiom]
forall a b. (a -> b) -> a -> b
$ [Named Axiom] -> ThSens Axiom Any
forall a b. Ord a => [Named a] -> ThSens a b
toThSens [Named Axiom]
sens)