Cross Reference: /hets/CommonLogic/OMDocExport.hs
OMDocExport.hs revision d2d5606ab65ddf48599bd044416de07a205095f2
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
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
b7de308d8bc28d42249256bddb16bbace71f60favboxsync{- |
b4f03aea544c9a58d8959658b31f7bd716a3f097vboxsyncModule : $Header$
5b281ba489ca18f0380d7efc7a5108b606cce449vboxsyncDescription : CommonLogic-to-OMDoc conversion
b4f03aea544c9a58d8959658b31f7bd716a3f097vboxsyncCopyright : (c) Iulia Ignatov, DFKI Bremen 2009, Eugen Kuksa, Uni Bremen 2011
b4f03aea544c9a58d8959658b31f7bd716a3f097vboxsyncLicense : GPLv2 or higher, see LICENSE.txt
b4f03aea544c9a58d8959658b31f7bd716a3f097vboxsync
1c94c0a63ba68be1a7b2c640e70d7a06464e4fcavboxsyncMaintainer : eugenk@informatik.uni-bremen.de
b4f03aea544c9a58d8959658b31f7bd716a3f097vboxsyncStability : experimental
b4f03aea544c9a58d8959658b31f7bd716a3f097vboxsyncPortability : portable
b4f03aea544c9a58d8959658b31f7bd716a3f097vboxsync
b4f03aea544c9a58d8959658b31f7bd716a3f097vboxsyncCommon Logic implementation of the interface functions
a16eb14ad7a4b5ef91ddc22d3e8e92d930f736fcvboxsyncexport_senToOmdoc and export_symToOmdoc from class Logic.
a16eb14ad7a4b5ef91ddc22d3e8e92d930f736fcvboxsyncThe actual instantiation can be found in module "CommonLogic.Logic_CommonLogic".
a16eb14ad7a4b5ef91ddc22d3e8e92d930f736fcvboxsync-}
a16eb14ad7a4b5ef91ddc22d3e8e92d930f736fcvboxsync
a16eb14ad7a4b5ef91ddc22d3e8e92d930f736fcvboxsyncmodule CommonLogic.OMDocExport
a16eb14ad7a4b5ef91ddc22d3e8e92d930f736fcvboxsync ( exportSymToOmdoc
a16eb14ad7a4b5ef91ddc22d3e8e92d930f736fcvboxsync , exportSenToOmdoc
a16eb14ad7a4b5ef91ddc22d3e8e92d930f736fcvboxsync ) where
a16eb14ad7a4b5ef91ddc22d3e8e92d930f736fcvboxsync
a16eb14ad7a4b5ef91ddc22d3e8e92d930f736fcvboxsyncimport CommonLogic.AS_CommonLogic as AS
a16eb14ad7a4b5ef91ddc22d3e8e92d930f736fcvboxsyncimport CommonLogic.Symbol
a16eb14ad7a4b5ef91ddc22d3e8e92d930f736fcvboxsyncimport CommonLogic.OMDoc
a16eb14ad7a4b5ef91ddc22d3e8e92d930f736fcvboxsync
1c94c0a63ba68be1a7b2c640e70d7a06464e4fcavboxsyncimport OMDoc.DataTypes
1c94c0a63ba68be1a7b2c640e70d7a06464e4fcavboxsync
1c94c0a63ba68be1a7b2c640e70d7a06464e4fcavboxsyncimport Common.Id
1c94c0a63ba68be1a7b2c640e70d7a06464e4fcavboxsyncimport Common.Result
b4f03aea544c9a58d8959658b31f7bd716a3f097vboxsync
b4f03aea544c9a58d8959658b31f7bd716a3f097vboxsyncimport qualified Data.Map as Map
cf57145d4697dceca3f0542b370c20f7a2c5c6e8vboxsync
cf57145d4697dceca3f0542b370c20f7a2c5c6e8vboxsync
b4f03aea544c9a58d8959658b31f7bd716a3f097vboxsynctype Env = NameMap Symbol
b4f03aea544c9a58d8959658b31f7bd716a3f097vboxsync
b4f03aea544c9a58d8959658b31f7bd716a3f097vboxsync-- | Exports the symbol @n@ to OMDoc
881b5ff6bc55e1fb0f4ef42f9782ccec79c0a138vboxsyncexportSymToOmdoc :: Env -> Symbol -> String -> Result TCElement
b4f03aea544c9a58d8959658b31f7bd716a3f097vboxsyncexportSymToOmdoc _ _ n = return $ TCSymbol n const_symbol Obj Nothing
590bfe12ce22cd3716448fbb9f4dc51664bfe5e2vboxsync
b4f03aea544c9a58d8959658b31f7bd716a3f097vboxsync
b4f03aea544c9a58d8959658b31f7bd716a3f097vboxsync-- | Exports the text @tm@ to OMDoc
b4f03aea544c9a58d8959658b31f7bd716a3f097vboxsyncexportSenToOmdoc :: Env -> TEXT_META
b4f03aea544c9a58d8959658b31f7bd716a3f097vboxsync -> Result TCorOMElement
b4f03aea544c9a58d8959658b31f7bd716a3f097vboxsyncexportSenToOmdoc en tm = return $ Right $ exportText en [] $ AS.getText tm
b4f03aea544c9a58d8959658b31f7bd716a3f097vboxsync
b4f03aea544c9a58d8959658b31f7bd716a3f097vboxsyncexportText :: Env -> [NAME_OR_SEQMARK] -> TEXT -> OMElement
b4f03aea544c9a58d8959658b31f7bd716a3f097vboxsyncexportText en vars txt = case txt of
b4f03aea544c9a58d8959658b31f7bd716a3f097vboxsync Text phrs _ ->
b4f03aea544c9a58d8959658b31f7bd716a3f097vboxsync OMA $ const_and : map (exportPhr en vars) (filter nonImportation phrs)
b4f03aea544c9a58d8959658b31f7bd716a3f097vboxsync Named_text n t _ ->
b4f03aea544c9a58d8959658b31f7bd716a3f097vboxsync OMA [const_textName, OMV $ mkSimpleName $ tokStr n, exportText en vars t]
b4f03aea544c9a58d8959658b31f7bd716a3f097vboxsync where nonImportation p = case p of
b4f03aea544c9a58d8959658b31f7bd716a3f097vboxsync Importation _ -> False
b4f03aea544c9a58d8959658b31f7bd716a3f097vboxsync _ -> True
b4f03aea544c9a58d8959658b31f7bd716a3f097vboxsync
b4f03aea544c9a58d8959658b31f7bd716a3f097vboxsyncexportPhr :: Env -> [NAME_OR_SEQMARK] -> PHRASE -> OMElement
b4f03aea544c9a58d8959658b31f7bd716a3f097vboxsyncexportPhr en vars phr = case phr of
b4f03aea544c9a58d8959658b31f7bd716a3f097vboxsync Importation _ -> undefined -- does not occur
b4f03aea544c9a58d8959658b31f7bd716a3f097vboxsync Module m -> OMBIND const_module [modName m] $ exportModule en vars m
b4f03aea544c9a58d8959658b31f7bd716a3f097vboxsync Sentence s -> exportSen en vars s
b4f03aea544c9a58d8959658b31f7bd716a3f097vboxsync Comment_text c t _ ->
b4f03aea544c9a58d8959658b31f7bd716a3f097vboxsync OMA [const_comment, varFromComment c, exportText en vars t]
b4f03aea544c9a58d8959658b31f7bd716a3f097vboxsync where modName m = case m of
b4f03aea544c9a58d8959658b31f7bd716a3f097vboxsync Mod n _ _ -> exportVar $ AS.Name n
b4f03aea544c9a58d8959658b31f7bd716a3f097vboxsync Mod_ex n _ _ _ -> exportVar $ AS.Name n
b4f03aea544c9a58d8959658b31f7bd716a3f097vboxsync
b4f03aea544c9a58d8959658b31f7bd716a3f097vboxsyncexportModule :: Env -> [NAME_OR_SEQMARK] -> MODULE -> OMElement
b4f03aea544c9a58d8959658b31f7bd716a3f097vboxsyncexportModule en vars m = case m of
b4f03aea544c9a58d8959658b31f7bd716a3f097vboxsync Mod _ t _ -> exportText en vars t
c5d2523548cc57504b829f53f1362b848a84542cvboxsync Mod_ex _ exs t _ -> OMA $ const_moduleExcludes : exportText en vars t
b4f03aea544c9a58d8959658b31f7bd716a3f097vboxsync : map (exportVar . AS.Name) exs
c5d2523548cc57504b829f53f1362b848a84542cvboxsync
c5d2523548cc57504b829f53f1362b848a84542cvboxsyncexportSen :: Env -> [NAME_OR_SEQMARK] -> SENTENCE
c5d2523548cc57504b829f53f1362b848a84542cvboxsync -> OMElement
b4f03aea544c9a58d8959658b31f7bd716a3f097vboxsyncexportSen en vars s = case s of
b4f03aea544c9a58d8959658b31f7bd716a3f097vboxsync Quant_sent qs _ -> case qs of
b4f03aea544c9a58d8959658b31f7bd716a3f097vboxsync QUANT_SENT q vars2 s2 -> OMBIND (case q of
b4f03aea544c9a58d8959658b31f7bd716a3f097vboxsync Universal -> const_forall
b4f03aea544c9a58d8959658b31f7bd716a3f097vboxsync Existential -> const_exists)
b4f03aea544c9a58d8959658b31f7bd716a3f097vboxsync (map exportVar vars2)
b4f03aea544c9a58d8959658b31f7bd716a3f097vboxsync (exportSen en (vars ++ vars2) s2)
b4f03aea544c9a58d8959658b31f7bd716a3f097vboxsync Bool_sent bs _ -> case bs of
b4f03aea544c9a58d8959658b31f7bd716a3f097vboxsync Junction j ss ->
b4f03aea544c9a58d8959658b31f7bd716a3f097vboxsync OMA $ (case j of Conjunction -> const_and
b4f03aea544c9a58d8959658b31f7bd716a3f097vboxsync Disjunction -> const_or)
b4f03aea544c9a58d8959658b31f7bd716a3f097vboxsync : map (exportSen en vars) ss
b4f03aea544c9a58d8959658b31f7bd716a3f097vboxsync Negation s1 -> OMA [ const_not, exportSen en vars s1]
b4f03aea544c9a58d8959658b31f7bd716a3f097vboxsync BinOp op s1 s2 -> OMA
b4f03aea544c9a58d8959658b31f7bd716a3f097vboxsync [ case op of Implication -> const_implies
b4f03aea544c9a58d8959658b31f7bd716a3f097vboxsync Biconditional -> const_equivalent
b4f03aea544c9a58d8959658b31f7bd716a3f097vboxsync , exportSen en vars s1
b4f03aea544c9a58d8959658b31f7bd716a3f097vboxsync , exportSen en vars s2]
31cda52093d58f5c604589fa74949c5fddcbde70vboxsync Atom_sent at _ -> case at of
31cda52093d58f5c604589fa74949c5fddcbde70vboxsync Equation t1 t2 -> OMA
31cda52093d58f5c604589fa74949c5fddcbde70vboxsync [ const_eq
31cda52093d58f5c604589fa74949c5fddcbde70vboxsync , exportTerm en vars t1
31cda52093d58f5c604589fa74949c5fddcbde70vboxsync , exportTerm en vars t2 ]
31cda52093d58f5c604589fa74949c5fddcbde70vboxsync Atom pt tts ->
31cda52093d58f5c604589fa74949c5fddcbde70vboxsync OMA $ exportTerm en vars pt : map (exportTermSeq en vars) tts
b4f03aea544c9a58d8959658b31f7bd716a3f097vboxsync Comment_sent _com s1 _ ->
b4f03aea544c9a58d8959658b31f7bd716a3f097vboxsync OMA [const_comment, varFromComment _com, exportSen en vars s1]
b4f03aea544c9a58d8959658b31f7bd716a3f097vboxsync Irregular_sent s1 _ ->
b4f03aea544c9a58d8959658b31f7bd716a3f097vboxsync OMA [const_irregular, exportSen en vars s1]
b4f03aea544c9a58d8959658b31f7bd716a3f097vboxsync
b4f03aea544c9a58d8959658b31f7bd716a3f097vboxsyncexportTerm :: Env -> [NAME_OR_SEQMARK] -> TERM -> OMElement
b4f03aea544c9a58d8959658b31f7bd716a3f097vboxsyncexportTerm e vars t = case t of
b4f03aea544c9a58d8959658b31f7bd716a3f097vboxsync Name_term n -> if AS.Name n `elem` vars
b4f03aea544c9a58d8959658b31f7bd716a3f097vboxsync then exportVar (AS.Name n)
b4f03aea544c9a58d8959658b31f7bd716a3f097vboxsync else oms e n
b4f03aea544c9a58d8959658b31f7bd716a3f097vboxsync Funct_term ft tss _ ->
b4f03aea544c9a58d8959658b31f7bd716a3f097vboxsync OMA $ exportTerm e vars ft : map (exportTermSeq e vars) tss
b4f03aea544c9a58d8959658b31f7bd716a3f097vboxsync Comment_term t1 _com _ ->
b4f03aea544c9a58d8959658b31f7bd716a3f097vboxsync OMA [ const_comment_term, varFromComment _com, exportTerm e vars t1 ]
b4f03aea544c9a58d8959658b31f7bd716a3f097vboxsync
8111a14f0afa014e5ec1cf1f010411772e10ebb4vboxsync
b4f03aea544c9a58d8959658b31f7bd716a3f097vboxsyncexportTermSeq :: Env -> [NAME_OR_SEQMARK] -> TERM_SEQ -> OMElement
b4f03aea544c9a58d8959658b31f7bd716a3f097vboxsyncexportTermSeq e vars ts = case ts of
b4f03aea544c9a58d8959658b31f7bd716a3f097vboxsync Term_seq t -> exportTerm e vars t
b4f03aea544c9a58d8959658b31f7bd716a3f097vboxsync Seq_marks s -> if SeqMark s `elem` vars
b4f03aea544c9a58d8959658b31f7bd716a3f097vboxsync then exportVar (SeqMark s)
31cda52093d58f5c604589fa74949c5fddcbde70vboxsync else oms e s
31cda52093d58f5c604589fa74949c5fddcbde70vboxsync
b4f03aea544c9a58d8959658b31f7bd716a3f097vboxsyncexportVar :: NAME_OR_SEQMARK -> OMElement
b4f03aea544c9a58d8959658b31f7bd716a3f097vboxsyncexportVar (AS.Name n) = OMV $ mkSimpleName $ tokStr n
b4f03aea544c9a58d8959658b31f7bd716a3f097vboxsyncexportVar (SeqMark s) = OMV $ mkSimpleName $ tokStr s
b4f03aea544c9a58d8959658b31f7bd716a3f097vboxsync
e5bfc5c34142a7550be3564a8e01a037b1db5b31vboxsyncvarFromComment :: COMMENT -> OMElement
e5bfc5c34142a7550be3564a8e01a037b1db5b31vboxsyncvarFromComment (Comment x _) = OMV $ mkSimpleName x
b4f03aea544c9a58d8959658b31f7bd716a3f097vboxsync
b4f03aea544c9a58d8959658b31f7bd716a3f097vboxsync
b4f03aea544c9a58d8959658b31f7bd716a3f097vboxsyncoms :: Env -> Token -> OMElement
b4f03aea544c9a58d8959658b31f7bd716a3f097vboxsyncoms e x =
b4f03aea544c9a58d8959658b31f7bd716a3f097vboxsync let s = toSymbol x
b4f03aea544c9a58d8959658b31f7bd716a3f097vboxsync err = error $ "oms: no mapping for the symbol " ++ show s
b4f03aea544c9a58d8959658b31f7bd716a3f097vboxsync -- printId1 (symName s) ++ "\n" ++ show e ++ "\n\n\n" ++ ""
b4f03aea544c9a58d8959658b31f7bd716a3f097vboxsync in simpleOMS $ findInEnv err e s
b4f03aea544c9a58d8959658b31f7bd716a3f097vboxsync
b4f03aea544c9a58d8959658b31f7bd716a3f097vboxsyncfindInEnv :: (Ord k) => a -> Map.Map k a -> k -> a
b4f03aea544c9a58d8959658b31f7bd716a3f097vboxsyncfindInEnv err m x = Map.findWithDefault err x m
b4f03aea544c9a58d8959658b31f7bd716a3f097vboxsync
b4f03aea544c9a58d8959658b31f7bd716a3f097vboxsync-- transform a NAME_OR_SEQMARK into a symbol.
b4f03aea544c9a58d8959658b31f7bd716a3f097vboxsynctoSymbol :: Token -> Symbol
b4f03aea544c9a58d8959658b31f7bd716a3f097vboxsynctoSymbol = Symbol . simpleIdToId
b4f03aea544c9a58d8959658b31f7bd716a3f097vboxsync