f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder{- |
e9458b1a7a19a63aa4c179f9ab20f4d50681c168Jens ElknerModule : ./OWL2/CreateOWL.hs
cb1afff56e051605acc301f23246126a9dc4a3a6Christian MaederDescription : translate theories to OWL2
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian MaederCopyright : (c) C. Maeder, DFKI GmbH 2012
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense : GPLv2 or higher, see LICENSE.txt
6a73412ec0da0b155b3fdce757d5699c34c37cc9Codruta Girlea
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian MaederMaintainer : Christian.Maeder@dfki.de
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian MaederStability : provisional
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian MaederPortability : non-portable (via Logic.Logic)
6a73412ec0da0b155b3fdce757d5699c34c37cc9Codruta Girlea-}
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder
6a73412ec0da0b155b3fdce757d5699c34c37cc9Codruta Girlea
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maedermodule OWL2.CreateOWL where
6a73412ec0da0b155b3fdce757d5699c34c37cc9Codruta Girlea
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maederimport Common.Result
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maederimport Common.AS_Annotation
6a73412ec0da0b155b3fdce757d5699c34c37cc9Codruta Girleaimport Logic.Coerce
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maederimport Logic.Comorphism
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder
6a73412ec0da0b155b3fdce757d5699c34c37cc9Codruta Girleaimport Static.GTheory
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maederimport Logic.Prover
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder
6a73412ec0da0b155b3fdce757d5699c34c37cc9Codruta Girleaimport Common.ExtSign
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maederimport OWL2.Sign
f5efb18d22fd7691109bd62426531dd8fe18064eCodruta Girleaimport OWL2.MS
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maederimport OWL2.Logic_OWL2
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maederimport OWL2.CASL2OWL
f5efb18d22fd7691109bd62426531dd8fe18064eCodruta Girleaimport OWL2.DMU2OWL2
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maederimport OWL2.Propositional2OWL2
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder
6a73412ec0da0b155b3fdce757d5699c34c37cc9Codruta Girleaimport CASL.Logic_CASL
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maederimport ExtModal.Logic_ExtModal
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maederimport Comorphisms.ExtModal2OWL
6a73412ec0da0b155b3fdce757d5699c34c37cc9Codruta Girlea
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maederimport DMU.Logic_DMU
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maederimport Propositional.Logic_Propositional
6a73412ec0da0b155b3fdce757d5699c34c37cc9Codruta Girlea
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian MaedercreateOWLTheory :: G_theory -> Result (Sign, [Named Axiom])
6a73412ec0da0b155b3fdce757d5699c34c37cc9Codruta GirleacreateOWLTheory (G_theory lid _ (ExtSign sign0 _) _ sens0 _) = do
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder let th = (sign0, toNamedList sens0)
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder r1 = coerceBasicTheory lid CASL "" th
6a73412ec0da0b155b3fdce757d5699c34c37cc9Codruta Girlea r1' = r1 >>= wrapMapTheory CASL2OWL
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder r2 = coerceBasicTheory lid DMU "" th
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder r2' = r2 >>= wrapMapTheory DMU2OWL2
f5efb18d22fd7691109bd62426531dd8fe18064eCodruta Girlea r3 = coerceBasicTheory lid Propositional "" th
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder r3' = r3 >>= wrapMapTheory Propositional2OWL2
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder r4 = coerceBasicTheory lid ExtModal "" th
f5efb18d22fd7691109bd62426531dd8fe18064eCodruta Girlea r4' = r4 >>= wrapMapTheory ExtModal2OWL
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder r5 = coerceBasicTheory lid OWL2 "" th
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder r6 = case maybeResult r1 of
f5efb18d22fd7691109bd62426531dd8fe18064eCodruta Girlea Nothing -> case maybeResult r2 of
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder Nothing -> case maybeResult r3 of
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder Nothing -> case maybeResult r4 of
f5efb18d22fd7691109bd62426531dd8fe18064eCodruta Girlea Nothing -> r5
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder _ -> r4'
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder _ -> r3'
f5efb18d22fd7691109bd62426531dd8fe18064eCodruta Girlea _ -> r2'
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder _ -> r1'
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder (sign, sens) <- r6
6679bc09e14a9495e9096fd26ada812b2f92ee63Codruta Girlea return (sign, toNamedList $ toThSens sens)
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder