null
CreateOWL.hs revision c1d06b3018b34ede2b3fb6c7fe2ad28cd5ce5b68
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{- |
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel ManceModule : $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
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel Mance
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel ManceMaintainer : Christian.Maeder@dfki.de
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel ManceStability : provisional
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel MancePortability : non-portable (via Logic.Logic)
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel Mance-}
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix 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
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel Manceimport 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
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel Mance
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel Mance
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel MancecreateOWLTheory :: G_theory -> Result (Sign, [Named Axiom])
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel MancecreateOWLTheory (G_theory lid _ (ExtSign sign0 _) _ sens0 _) = do
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel Mance 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
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel Mance r3 = coerceBasicTheory lid Propositional "" th
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel Mance 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'
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel Mance _ -> r2'
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel Mance _ -> r1'
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel Mance (sign, sens) <- r6
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel Mance return (sign, toNamedList $ toThSens sens)
f501e448d92c4d819b6bfc1d6487da76cf22528cFelix Gabriel Mance