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