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
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaederDescription : json output of Hets development graphs
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaederCopyright : (c) Christian Maeder, DFKI GmbH 2014
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaederLicense : GPLv2 or higher, see LICENSE.txt
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaederMaintainer : Christian.Maeder@dfki.de
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaederStability : provisional
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaederPortability : non-portable(Grothendieck)
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaederJson of Hets DGs
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaeder , dgSymbols
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa , declarations
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaeder , showSymbols
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaeder , showSymbolsTh
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaederimport Static.ComputeTheory (getImportNames)
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaederimport qualified Common.OrderedMap as OMap
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaederimport qualified Data.Map as Map
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaederimport qualified Data.Set as Set (toList)
3aa46bd44769d35fe889134a94be25bdae650890cmaederExport the development graph as json. If the flag full is True then
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaedersymbols for all nodes are shown as declarations, otherwise (the
3aa46bd44769d35fe889134a94be25bdae650890cmaederdefault) only declaration for basic spec nodes are shown as is done
3aa46bd44769d35fe889134a94be25bdae650890cmaederfor the corresponding xml output. -}
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaederdGraph :: HetcatsOpts -> LibEnv -> LibName -> DGraph -> Json
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksadGraph opts lenv ln dg =
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaeder let body = dgBody dg
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaeder ga = globalAnnos dg
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaeder lnodes = labNodes body
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaeder ledges = labEdges body
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaeder in tagJson "DGraph" $ mkJObj
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaeder [ mkJPair "filename" $ getFilePath ln
3aa46bd44769d35fe889134a94be25bdae650890cmaeder , mkJPair "mime-type" . fromMaybe "unknown" $ mimeType ln
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaeder , mkJPair "libname" . show $ setAngles False $ getLibId ln
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaeder , ("dgnodes", mkJNum $ length lnodes)
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaeder , ("dgedges", mkJNum $ length ledges)
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaeder , ("nextlinkid", mkJNum . getEdgeNum $ getNewEdgeId dg)
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaeder , ("Global", mkJArr . map (anToJson ga) . convertGlobalAnnos
46c318705d1532d90572abf9ee869016583d985bTill Mossakowski $ removeDOLprefixes ga)
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa , ("DGNode", mkJArr $ map (lnode opts ga lenv) lnodes)
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa , ("DGLink", mkJArr $ map (ledge opts ga dg) ledges) ]
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaedergmorph :: HetcatsOpts -> GlobalAnnos -> GMorphism -> Json
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaedergmorph opts ga gm@(GMorphism cid (ExtSign ssig _) _ tmor _) =
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaeder case map_sign cid ssig of
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaeder Result _ mr -> case mr of
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaeder Nothing -> error $ "Static.ToXml.gmorph: " ++ showGlobalDoc ga gm ""
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaeder Just (tsig, tsens) -> let
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaeder tid = targetLogic cid
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaeder sl = Map.toList . Map.filterWithKey (/=) $ symmap_of tid tmor
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaeder $ mkNameJPair (language_name cid)
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaeder : [("ComorphismAxioms", mkJArr
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa $ map (showSen opts (targetLogic cid) ga Nothing tsig) tsens)
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaeder | not (fullTheories opts) && not (null tsens) ]
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaeder ++ [("Map", mkJArr $
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaeder map (\ (s, t) -> mkJObj
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaeder [("map", showSym tid s), ("to", showSym tid t)]) sl)
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaeder | not $ null sl]
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaederprettySymbol :: (GetRange a, Pretty a) => GlobalAnnos -> a -> [JPair]
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaederprettySymbol = rangedToJson "Symbol"
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaederlnode :: HetcatsOpts -> GlobalAnnos -> LibEnv -> LNode DGNodeLab -> Json
a2e63acda4b7d52f3f0d6fef6d30d0fe660a28b1ysengrimmlnode opts ga lenv (nodeId, lbl) =
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaeder let nm = dgn_name lbl
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaeder (spn, xp) = case reverse $ xpath nm of
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaeder ElemName s : t -> (s, showXPath t)
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaeder l -> ("?", showXPath l)
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaeder $ mkNameJPair (showName nm)
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaeder : rangeToJPair (srcRange nm)
a2e63acda4b7d52f3f0d6fef6d30d0fe660a28b1ysengrimm ++ [("id", mkJNum nodeId)]
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaeder ++ [("reference", mkJBool $ isDGRef lbl)]
85688faec4e22ab1b6d328415e47063a42b98ec0ysengrimm ++ [("internal", mkJBool $ isInternal nm)]
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaeder ++ case signOf $ dgn_theory lbl of
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaeder G_sign slid _ _ -> mkJPair "logic" (show slid)
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaeder : if not (isDGRef lbl) && dgn_origin lbl < DGProof then
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaeder [mkJPair "refname" spn, mkJPair "relxpath" xp ]
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaeder ++ case nodeInfo lbl of
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaeder DGRef li rf ->
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaeder [ ("Reference", mkJObj
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaeder [ mkJPair "library" $ show $ setAngles False $ getLibId li
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaeder , mkJPair "location" $ getFilePath li
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaeder , mkJPair "node" $ getNameOfNode rf $ lookupDGraph li lenv ])]
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaeder DGNode orig cs -> consStatus cs ++ case orig of
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaeder DGBasicSpec _ (G_sign lid (ExtSign dsig _) _) _ ->
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaeder let syms = mostSymsOf lid dsig in
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa [ ("Declarations", declarations lid syms)
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa | not $ null syms ]
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaeder DGRestriction _ hidSyms ->
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaeder [ ("Hidden", mkJArr
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaeder . map (mkJObj . prettySymbol ga)
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaeder ++ case dgn_theory lbl of
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa G_theory lid _ extSig@(ExtSign sig _) _ thsens _ -> let
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaeder (axs, thms) = OMap.partition isAxiom thsens
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaeder nAxs = toNamedList axs
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa [("Symbols", symbols lid extSig)
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa | fullSign opts ]
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaeder ++ [("Axioms", mkJArr
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa $ map (showSen opts lid ga Nothing sig) nAxs) | not $ null nAxs ]
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaeder ++ [("Theorems", mkJArr
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa $ map (\ (s, t) -> showSen opts lid ga
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaeder (Just $ isProvenSenStatus t) sig $ toNamed s t)
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaeder nThms) | not $ null nThms]
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa ++ if fullTheories opts then case globalTheory lbl of
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaeder Just (G_theory glid _ _ _ allSens _) -> case
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaeder coerceThSens glid lid "xml-lnode" allSens of
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaeder Just gsens -> let
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaeder nSens = toNamedList
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaeder $ OMap.filter ((`notElem` map sentence
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaeder (OMap.elems thsens)) . sentence) gsens
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaeder in [("ImpAxioms", mkJArr
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa $ map (showSen opts lid ga Nothing sig) nSens)
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaeder | not $ null nSens ]
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaeder-- | a status may be open, proven or outdated
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaedermkStatusJPair :: String -> JPair
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaedermkStatusJPair = mkJPair "status"
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaedermkProvenJPair :: Bool -> JPair
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaedermkProvenJPair b = mkStatusJPair $ if b then "proven" else "open"
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaederconsStatus :: ConsStatus -> [JPair]
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaederconsStatus cs = case getConsOfStatus cs of
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaeder cStat -> [("ConsStatus", mkJStr $ show cStat)]
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaederledge :: HetcatsOpts -> GlobalAnnos -> DGraph -> LEdge DGLinkLab -> Json
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaederledge opts ga dg (f, t, lbl) = let
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaeder typ = dgl_type lbl
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaeder mor = gmorph opts ga $ dgl_morphism lbl
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaeder mkMor n = [mkJPair "morphismsource" $ getNameOfNode n dg]
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaeder lnkSt = case thmLinkStatus typ of
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaeder Nothing -> []
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaeder Just tls -> case tls of
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaeder LeftOpen -> []
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaeder Proven r ls -> dgrule r
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaeder ++ let bs = Set.toList $ proofBasis ls in
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaeder [("ProofBasis", mkJArr
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaeder $ map (mkJNum . getEdgeNum) bs) | not $ null bs]
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaeder $ [ mkJPair "source" $ getNameOfNode f dg
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaeder , mkJPair "target" $ getNameOfNode t dg
842df3191c25c4207098f1a0302ed892098ec523ysengrimm , ("linkid", mkJNum . getEdgeNum $ dgl_id lbl)
842df3191c25c4207098f1a0302ed892098ec523ysengrimm , ("id_source", mkJNum f)
842df3191c25c4207098f1a0302ed892098ec523ysengrimm , ("id_target", mkJNum t) ]
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaeder ++ case dgl_origin lbl of
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaeder DGLinkView i _ ->
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaeder [mkNameJPair . iriToStringShortUnsecure $ setAngles False i]
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaeder ++ mkJPair "Type" (getDGLinkType lbl) : lnkSt
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaeder ++ consStatus (getLinkConsStatus typ)
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaeder ++ case typ of
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaeder HidingFreeOrCofreeThm _ n _ _ -> mkMor n
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaeder FreeOrCofreeDefLink _ (JustNode ns) -> mkMor $ getNode ns
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaeder ++ [("GMorphism", mor)]
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaederdgrule :: DGRule -> [JPair]
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaeder mkJPair "Rule" (dgRuleHeader r)
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaeder : case r of
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaeder DGRuleLocalInference m -> [("MovedTheorems", mkJArr
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaeder $ map (\ (s, t) -> mkJObj [mkNameJPair s, mkJPair "renamedTo" t]) m)]
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaeder Composition es ->
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaeder [("Composition", mkJArr $ map (mkJNum . getEdgeNum) es)]
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaeder DGRuleWithEdge _ e -> [("RuleTarget", mkJNum $ getEdgeNum e)]
3aa46bd44769d35fe889134a94be25bdae650890cmaeder-- | collects all symbols from dg and displays them as json
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksadgSymbols :: HetcatsOpts -> DGraph -> Json
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksadgSymbols opts dg = let ga = globalAnnos dg in tagJson "Ontologies"
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaeder $ mkJArr $ map (\ (i, lbl) -> let ins = getImportNames dg i in
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa showSymbols opts ins ga lbl) $ labNodesDG dg
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksashowSymbols :: HetcatsOpts -> [String] -> GlobalAnnos -> DGNodeLab -> Json
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksashowSymbols opts ins ga lbl = showSymbolsTh opts ins (getDGNodeName lbl) ga
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaeder $ dgn_theory lbl
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksashowSymbolsTh :: HetcatsOpts -> [String] -> String -> GlobalAnnos -> G_theory -> Json
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksashowSymbolsTh opts ins name ga th = case th of
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaeder G_theory lid _ (ExtSign sig _) _ sens _ -> mkJObj
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaeder [ mkJPair "logic" $ language_name lid
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaeder , mkNameJPair name
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaeder , ("Ontology", mkJObj
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaeder [ ("Symbols", mkJArr . map (showSym lid) $ symlist_of lid sig)
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa , ("Axioms", mkJArr . map (showSen opts lid ga Nothing sig)
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaeder $ toNamedList sens)
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaeder , ("Import", mkJArr $ map mkJStr ins) ])]
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaedershowSen :: ( GetRange sentence, Pretty sentence
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaeder , Sentences lid sentence sign morphism symbol) =>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa HetcatsOpts -> lid -> GlobalAnnos -> Maybe Bool -> sign -> Named sentence -> Json
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksashowSen opts lid ga mt sig ns = let s = sentence ns in mkJObj
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaeder $ case mt of
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaeder Nothing -> []
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaeder Just b -> [mkProvenJPair b]
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaeder ++ mkNameJPair (senAttr ns) : rangeToJPair (getRangeSpan s)
9a251d18898bb5244e0f0128c4824d046b01f84emcodescu ++ case priority ns of
6c5825dc6324f6572cdc407b69afd59942182389mcodescu Just p -> [mkPriorityJPair p]
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaeder ++ mkJPair (if isJust mt then "Theorem" else "Axiom")
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaeder (show . useGlobalAnnos ga . print_named lid
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaeder . makeNamed "" $ simplify_sen lid sig s)
a7338b15cbc9b513aaded07198c8666f0fa9d612Till Mossakowski : (let syms = symsOfSen lid sig s in
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaeder [("SenSymbols", mkJArr $ map (showSym lid) syms)
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaeder | not $ null syms])
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaeder ++ case senMark ns of
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaeder m -> [mkJPair "ComorphismOrigin" m]
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa ++ if printAST opts
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa then [("AST", asJson s)]
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksadeclarations :: Sentences lid sentence sign morphism symbol
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa => lid -> [symbol] -> Json
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksadeclarations lid syms = mkJArr $ map (showSym lid) syms
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksasymbols :: Sentences lid sentence sign morphism symbol
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa => lid -> ExtSign sign symbol -> Json
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksasymbols lid (ExtSign sig _) = mkJArr . map (showSym lid) $ symlist_of lid sig
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaedershowSym :: Sentences lid sentence sign morphism symbol => lid -> symbol -> Json
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaedershowSym lid s = mkJObj
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaeder $ [ mkJPair "kind" $ symKind lid s
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaeder , mkNameJPair . show $ sym_name lid s
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaeder , mkJPair "iri" $ fullSymName lid s ]
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaeder ++ prettySymbol emptyGlobalAnnos s