Cross Reference: /hets/OWL2/CreateOWL.hs
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
32607d06fe7826eb0711c19d348ee4e395f2577aChristian Maeder{- |
e9458b1a7a19a63aa4c179f9ab20f4d50681c168Jens ElknerModule : ./OWL2/CreateOWL.hs
32607d06fe7826eb0711c19d348ee4e395f2577aChristian MaederDescription : translate theories to OWL2
32607d06fe7826eb0711c19d348ee4e395f2577aChristian MaederCopyright : (c) C. Maeder, DFKI GmbH 2012
32607d06fe7826eb0711c19d348ee4e395f2577aChristian MaederLicense : GPLv2 or higher, see LICENSE.txt
32607d06fe7826eb0711c19d348ee4e395f2577aChristian Maeder
32607d06fe7826eb0711c19d348ee4e395f2577aChristian MaederMaintainer : Christian.Maeder@dfki.de
32607d06fe7826eb0711c19d348ee4e395f2577aChristian MaederStability : provisional
32607d06fe7826eb0711c19d348ee4e395f2577aChristian MaederPortability : non-portable (via Logic.Logic)
32607d06fe7826eb0711c19d348ee4e395f2577aChristian Maeder-}
32607d06fe7826eb0711c19d348ee4e395f2577aChristian Maeder
32607d06fe7826eb0711c19d348ee4e395f2577aChristian Maeder
32607d06fe7826eb0711c19d348ee4e395f2577aChristian Maedermodule OWL2.CreateOWL where
32607d06fe7826eb0711c19d348ee4e395f2577aChristian Maeder
32607d06fe7826eb0711c19d348ee4e395f2577aChristian Maederimport Common.Result
32607d06fe7826eb0711c19d348ee4e395f2577aChristian Maederimport Common.AS_Annotation
32607d06fe7826eb0711c19d348ee4e395f2577aChristian Maederimport Logic.Coerce
32607d06fe7826eb0711c19d348ee4e395f2577aChristian Maederimport Logic.Comorphism
32607d06fe7826eb0711c19d348ee4e395f2577aChristian Maeder
32607d06fe7826eb0711c19d348ee4e395f2577aChristian Maederimport Static.GTheory
32607d06fe7826eb0711c19d348ee4e395f2577aChristian Maederimport Logic.Prover
32607d06fe7826eb0711c19d348ee4e395f2577aChristian Maeder
32607d06fe7826eb0711c19d348ee4e395f2577aChristian Maederimport Common.ExtSign
32607d06fe7826eb0711c19d348ee4e395f2577aChristian Maeder
32607d06fe7826eb0711c19d348ee4e395f2577aChristian Maederimport OWL2.Sign
32607d06fe7826eb0711c19d348ee4e395f2577aChristian Maederimport OWL2.MS
32607d06fe7826eb0711c19d348ee4e395f2577aChristian Maederimport OWL2.Logic_OWL2
32607d06fe7826eb0711c19d348ee4e395f2577aChristian Maederimport OWL2.CASL2OWL
32607d06fe7826eb0711c19d348ee4e395f2577aChristian Maederimport OWL2.DMU2OWL2
32607d06fe7826eb0711c19d348ee4e395f2577aChristian Maederimport OWL2.Propositional2OWL2
32607d06fe7826eb0711c19d348ee4e395f2577aChristian Maeder
32607d06fe7826eb0711c19d348ee4e395f2577aChristian Maederimport CASL.Logic_CASL
32607d06fe7826eb0711c19d348ee4e395f2577aChristian Maederimport ExtModal.Logic_ExtModal
32607d06fe7826eb0711c19d348ee4e395f2577aChristian Maederimport Comorphisms.ExtModal2OWL
32607d06fe7826eb0711c19d348ee4e395f2577aChristian Maeder
32607d06fe7826eb0711c19d348ee4e395f2577aChristian Maederimport DMU.Logic_DMU
32607d06fe7826eb0711c19d348ee4e395f2577aChristian Maederimport Propositional.Logic_Propositional
32607d06fe7826eb0711c19d348ee4e395f2577aChristian Maeder
32607d06fe7826eb0711c19d348ee4e395f2577aChristian Maeder
32607d06fe7826eb0711c19d348ee4e395f2577aChristian MaedercreateOWLTheory :: G_theory -> Result (Sign, [Named Axiom])
c1d06b3018b34ede2b3fb6c7fe2ad28cd5ce5b68Christian MaedercreateOWLTheory (G_theory lid _ (ExtSign sign0 _) _ sens0 _) = do
32607d06fe7826eb0711c19d348ee4e395f2577aChristian Maeder let th = (sign0, toNamedList sens0)
32607d06fe7826eb0711c19d348ee4e395f2577aChristian Maeder r1 = coerceBasicTheory lid CASL "" th
32607d06fe7826eb0711c19d348ee4e395f2577aChristian Maeder r1' = r1 >>= wrapMapTheory CASL2OWL
32607d06fe7826eb0711c19d348ee4e395f2577aChristian Maeder r2 = coerceBasicTheory lid DMU "" th
32607d06fe7826eb0711c19d348ee4e395f2577aChristian Maeder r2' = r2 >>= wrapMapTheory DMU2OWL2
32607d06fe7826eb0711c19d348ee4e395f2577aChristian Maeder r3 = coerceBasicTheory lid Propositional "" th
32607d06fe7826eb0711c19d348ee4e395f2577aChristian Maeder r3' = r3 >>= wrapMapTheory Propositional2OWL2
32607d06fe7826eb0711c19d348ee4e395f2577aChristian Maeder r4 = coerceBasicTheory lid ExtModal "" th
32607d06fe7826eb0711c19d348ee4e395f2577aChristian Maeder r4' = r4 >>= wrapMapTheory ExtModal2OWL
32607d06fe7826eb0711c19d348ee4e395f2577aChristian Maeder r5 = coerceBasicTheory lid OWL2 "" th
32607d06fe7826eb0711c19d348ee4e395f2577aChristian Maeder r6 = case maybeResult r1 of
32607d06fe7826eb0711c19d348ee4e395f2577aChristian Maeder Nothing -> case maybeResult r2 of
32607d06fe7826eb0711c19d348ee4e395f2577aChristian Maeder Nothing -> case maybeResult r3 of
32607d06fe7826eb0711c19d348ee4e395f2577aChristian Maeder Nothing -> case maybeResult r4 of
32607d06fe7826eb0711c19d348ee4e395f2577aChristian Maeder Nothing -> r5
32607d06fe7826eb0711c19d348ee4e395f2577aChristian Maeder _ -> r4'
32607d06fe7826eb0711c19d348ee4e395f2577aChristian Maeder _ -> r3'
32607d06fe7826eb0711c19d348ee4e395f2577aChristian Maeder _ -> r2'
32607d06fe7826eb0711c19d348ee4e395f2577aChristian Maeder _ -> r1'
32607d06fe7826eb0711c19d348ee4e395f2577aChristian Maeder (sign, sens) <- r6
c505f62dff03727dc14a1f08be48208540d78d4aChristian Maeder return (sign, toNamedList $ toThSens sens)