Cross Reference: /hets/OWL2/CreateOWL.hs
CreateOWL.hs revision c505f62dff03727dc14a1f08be48208540d78d4a
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
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel Mance{- |
e9458b1a7a19a63aa4c179f9ab20f4d50681c168Jens ElknerModule : $Header$
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel ManceDescription : translate theories to OWL2
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel ManceCopyright : (c) C. Maeder, DFKI GmbH 2012
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel ManceLicense : GPLv2 or higher, see LICENSE.txt
fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel ManceMaintainer : Christian.Maeder@dfki.de
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel ManceStability : provisional
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel MancePortability : non-portable (via Logic.Logic)
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel Mance-}
68ace74bf7cd65cb7eb7e19ffe373520fc520e0cFelix Gabriel Mance
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel Mance
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel Mancemodule OWL2.CreateOWL where
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel Mance
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel Manceimport Common.Result
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel Manceimport Common.AS_Annotation
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel Manceimport Logic.Coerce
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel Manceimport Logic.Comorphism
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel Mance
80875f917d741946a39d0ec0b5721e46ba609823Till Mossakowskiimport Static.GTheory
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel Manceimport Logic.Prover
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel Mance
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel Manceimport Common.ExtSign
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel Mance
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel Manceimport OWL2.Sign
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel Manceimport OWL2.MS
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel Manceimport OWL2.Logic_OWL2
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel Manceimport OWL2.CASL2OWL
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel Manceimport OWL2.DMU2OWL2
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel Manceimport OWL2.Propositional2OWL2
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel Mance
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel Manceimport CASL.Logic_CASL
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel Manceimport ExtModal.Logic_ExtModal
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel Manceimport Comorphisms.ExtModal2OWL
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel Mance
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel Manceimport DMU.Logic_DMU
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel Manceimport Propositional.Logic_Propositional
7a443a42affdb218b848a9d6b58a4d7675c1c543Felix Gabriel Mance
7a443a42affdb218b848a9d6b58a4d7675c1c543Felix Gabriel Mance
732014c1519f1087a7fed3316969b21537394b77Christian MaedercreateOWLTheory :: G_theory -> Result (Sign, [Named Axiom])
f6f50c832e59d06ae11bbfcf94d0df87313c844eFelix Gabriel MancecreateOWLTheory (G_theory lid (ExtSign sign0 _) _ sens0 _) = do
51be3b318544e318688bc3f8ee41e21b765dba61Mihai Codescu let th = (sign0, toNamedList sens0)
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel Mance r1 = coerceBasicTheory lid CASL "" th
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel Mance r1' = r1 >>= wrapMapTheory CASL2OWL
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel Mance r2 = coerceBasicTheory lid DMU "" th
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel Mance r2' = r2 >>= wrapMapTheory DMU2OWL2
7a443a42affdb218b848a9d6b58a4d7675c1c543Felix Gabriel Mance r3 = coerceBasicTheory lid Propositional "" th
732014c1519f1087a7fed3316969b21537394b77Christian Maeder r3' = r3 >>= wrapMapTheory Propositional2OWL2
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel Mance r4 = coerceBasicTheory lid ExtModal "" th
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel Mance r4' = r4 >>= wrapMapTheory ExtModal2OWL
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel Mance r5 = coerceBasicTheory lid OWL2 "" th
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel Mance r6 = case maybeResult r1 of
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel Mance Nothing -> case maybeResult r2 of
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel Mance Nothing -> case maybeResult r3 of
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel Mance Nothing -> case maybeResult r4 of
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel Mance Nothing -> r5
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel Mance _ -> r4'
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel Mance _ -> r3'
7a443a42affdb218b848a9d6b58a4d7675c1c543Felix Gabriel Mance _ -> r2'
7a443a42affdb218b848a9d6b58a4d7675c1c543Felix Gabriel Mance _ -> r1'
7a443a42affdb218b848a9d6b58a4d7675c1c543Felix Gabriel Mance (sign, sens) <- r6
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel Mance return (sign, toNamedList $ toThSens sens)
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel Mance