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
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
1c94c0a63ba68be1a7b2c640e70d7a06464e4fcavboxsyncMaintainer : eugenk@informatik.uni-bremen.de
b4f03aea544c9a58d8959658b31f7bd716a3f097vboxsyncStability : experimental
b4f03aea544c9a58d8959658b31f7bd716a3f097vboxsyncPortability : portable
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 ( exportSymToOmdoc
a16eb14ad7a4b5ef91ddc22d3e8e92d930f736fcvboxsync , exportSenToOmdoc
b4f03aea544c9a58d8959658b31f7bd716a3f097vboxsyncimport qualified Data.Map as Map
b4f03aea544c9a58d8959658b31f7bd716a3f097vboxsynctype Env = NameMap Symbol
b4f03aea544c9a58d8959658b31f7bd716a3f097vboxsync-- | Exports the symbol @n@ to OMDoc
881b5ff6bc55e1fb0f4ef42f9782ccec79c0a138vboxsyncexportSymToOmdoc :: Env -> Symbol -> String -> Result TCElement
b4f03aea544c9a58d8959658b31f7bd716a3f097vboxsyncexportSymToOmdoc _ _ n = return $ TCSymbol n const_symbol Obj Nothing
b4f03aea544c9a58d8959658b31f7bd716a3f097vboxsync-- | Exports the text @tm@ to OMDoc
b4f03aea544c9a58d8959658b31f7bd716a3f097vboxsyncexportSenToOmdoc :: Env -> TEXT_META
b4f03aea544c9a58d8959658b31f7bd716a3f097vboxsync -> Result TCorOMElement
b4f03aea544c9a58d8959658b31f7bd716a3f097vboxsyncexportSenToOmdoc en tm = return $ Right $ exportText en [] $ AS.getText tm
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
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
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
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 , 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]
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 ]
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
b4f03aea544c9a58d8959658b31f7bd716a3f097vboxsyncexportVar :: NAME_OR_SEQMARK -> OMElement
b4f03aea544c9a58d8959658b31f7bd716a3f097vboxsyncexportVar (AS.Name n) = OMV $ mkSimpleName $ tokStr n
b4f03aea544c9a58d8959658b31f7bd716a3f097vboxsyncexportVar (SeqMark s) = OMV $ mkSimpleName $ tokStr s
e5bfc5c34142a7550be3564a8e01a037b1db5b31vboxsyncvarFromComment :: COMMENT -> OMElement
e5bfc5c34142a7550be3564a8e01a037b1db5b31vboxsyncvarFromComment (Comment x _) = OMV $ mkSimpleName x
b4f03aea544c9a58d8959658b31f7bd716a3f097vboxsyncoms :: Env -> Token -> OMElement
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
b4f03aea544c9a58d8959658b31f7bd716a3f097vboxsyncfindInEnv :: (Ord k) => a -> Map.Map k a -> k -> a
b4f03aea544c9a58d8959658b31f7bd716a3f097vboxsyncfindInEnv err m x = Map.findWithDefault err x m
b4f03aea544c9a58d8959658b31f7bd716a3f097vboxsync-- transform a NAME_OR_SEQMARK into a symbol.
b4f03aea544c9a58d8959658b31f7bd716a3f097vboxsynctoSymbol :: Token -> Symbol
b4f03aea544c9a58d8959658b31f7bd716a3f097vboxsynctoSymbol = Symbol . simpleIdToId