{- |
Module      :  ./Static/ToJson.hs
Description :  json output of Hets development graphs
Copyright   :  (c) Christian Maeder, DFKI GmbH 2014
License     :  GPLv2 or higher, see LICENSE.txt
Maintainer  :  Christian.Maeder@dfki.de
Stability   :  provisional
Portability :  non-portable(Grothendieck)

Json of Hets DGs
-}

module Static.ToJson
  ( dGraph
  , lnode
  , gmorph
  , dgSymbols
  , declarations
  , symbols
  , showSymbols
  , showSymbolsTh
  ) where

import Driver.Options

import Static.DgUtils
import Static.DevGraph
import Static.GTheory
import Static.ComputeTheory (getImportNames)
import Static.PrintDevGraph

import Logic.Prover
import Logic.Logic
import Logic.Comorphism
import Logic.Grothendieck

import Common.AS_Annotation
import Common.ConvertGlobalAnnos
import Common.Consistency
import Common.DocUtils
import Common.ExtSign
import Common.GlobalAnnotations
import Common.Id
import Common.IRI
import Common.LibName
import qualified Common.OrderedMap as OMap
import Common.Result
import Common.Json

import Data.Graph.Inductive.Graph as Graph
import Data.Maybe
import qualified Data.Map as Map
import qualified Data.Set as Set (toList)

{- |
Export the development graph as json. If the flag full is True then
symbols for all nodes are shown as declarations, otherwise (the
default) only declaration for basic spec nodes are shown as is done
for the corresponding xml output. -}
dGraph :: HetcatsOpts -> LibEnv -> LibName -> DGraph -> Json
dGraph :: HetcatsOpts -> LibEnv -> LibName -> DGraph -> Json
dGraph opts :: HetcatsOpts
opts lenv :: LibEnv
lenv ln :: LibName
ln dg :: DGraph
dg =
  let body :: Gr DGNodeLab DGLinkLab
body = DGraph -> Gr DGNodeLab DGLinkLab
dgBody DGraph
dg
      ga :: GlobalAnnos
ga = DGraph -> GlobalAnnos
globalAnnos DGraph
dg
      lnodes :: [LNode DGNodeLab]
lnodes = Gr DGNodeLab DGLinkLab -> [LNode DGNodeLab]
forall (gr :: * -> * -> *) a b. Graph gr => gr a b -> [LNode a]
labNodes Gr DGNodeLab DGLinkLab
body
      ledges :: [LEdge DGLinkLab]
ledges = Gr DGNodeLab DGLinkLab -> [LEdge DGLinkLab]
forall (gr :: * -> * -> *) a b. Graph gr => gr a b -> [LEdge b]
labEdges Gr DGNodeLab DGLinkLab
body
  in String -> Json -> Json
tagJson "DGraph" (Json -> Json) -> Json -> Json
forall a b. (a -> b) -> a -> b
$ [JPair] -> Json
mkJObj
         [ String -> String -> JPair
mkJPair "filename" (String -> JPair) -> String -> JPair
forall a b. (a -> b) -> a -> b
$ LibName -> String
getFilePath LibName
ln
         , String -> String -> JPair
mkJPair "mime-type" (String -> JPair)
-> (Maybe String -> String) -> Maybe String -> JPair
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Maybe String -> String
forall a. a -> Maybe a -> a
fromMaybe "unknown" (Maybe String -> JPair) -> Maybe String -> JPair
forall a b. (a -> b) -> a -> b
$ LibName -> Maybe String
mimeType LibName
ln
         , String -> String -> JPair
mkJPair "libname" (String -> JPair) -> (IRI -> String) -> IRI -> JPair
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IRI -> String
forall a. Show a => a -> String
show (IRI -> JPair) -> IRI -> JPair
forall a b. (a -> b) -> a -> b
$ Bool -> IRI -> IRI
setAngles Bool
False (IRI -> IRI) -> IRI -> IRI
forall a b. (a -> b) -> a -> b
$ LibName -> IRI
getLibId LibName
ln
         , ("dgnodes", Int -> Json
forall b. Real b => b -> Json
mkJNum (Int -> Json) -> Int -> Json
forall a b. (a -> b) -> a -> b
$ [LNode DGNodeLab] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [LNode DGNodeLab]
lnodes)
         , ("dgedges", Int -> Json
forall b. Real b => b -> Json
mkJNum (Int -> Json) -> Int -> Json
forall a b. (a -> b) -> a -> b
$ [LEdge DGLinkLab] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [LEdge DGLinkLab]
ledges)
         , ("nextlinkid", Int -> Json
forall b. Real b => b -> Json
mkJNum (Int -> Json) -> (EdgeId -> Int) -> EdgeId -> Json
forall b c a. (b -> c) -> (a -> b) -> a -> c
. EdgeId -> Int
getEdgeNum (EdgeId -> Json) -> EdgeId -> Json
forall a b. (a -> b) -> a -> b
$ DGraph -> EdgeId
getNewEdgeId DGraph
dg)
         , ("Global", [Json] -> Json
mkJArr ([Json] -> Json) -> (GlobalAnnos -> [Json]) -> GlobalAnnos -> Json
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Annotation -> Json) -> [Annotation] -> [Json]
forall a b. (a -> b) -> [a] -> [b]
map (GlobalAnnos -> Annotation -> Json
anToJson GlobalAnnos
ga) ([Annotation] -> [Json])
-> (GlobalAnnos -> [Annotation]) -> GlobalAnnos -> [Json]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GlobalAnnos -> [Annotation]
convertGlobalAnnos
                            (GlobalAnnos -> Json) -> GlobalAnnos -> Json
forall a b. (a -> b) -> a -> b
$ GlobalAnnos -> GlobalAnnos
removeDOLprefixes GlobalAnnos
ga)
         , ("DGNode", [Json] -> Json
mkJArr ([Json] -> Json) -> [Json] -> Json
forall a b. (a -> b) -> a -> b
$ (LNode DGNodeLab -> Json) -> [LNode DGNodeLab] -> [Json]
forall a b. (a -> b) -> [a] -> [b]
map (HetcatsOpts -> GlobalAnnos -> LibEnv -> LNode DGNodeLab -> Json
lnode HetcatsOpts
opts GlobalAnnos
ga LibEnv
lenv) [LNode DGNodeLab]
lnodes)
         , ("DGLink", [Json] -> Json
mkJArr ([Json] -> Json) -> [Json] -> Json
forall a b. (a -> b) -> a -> b
$ (LEdge DGLinkLab -> Json) -> [LEdge DGLinkLab] -> [Json]
forall a b. (a -> b) -> [a] -> [b]
map (HetcatsOpts -> GlobalAnnos -> DGraph -> LEdge DGLinkLab -> Json
ledge HetcatsOpts
opts GlobalAnnos
ga DGraph
dg) [LEdge DGLinkLab]
ledges) ]

gmorph :: HetcatsOpts -> GlobalAnnos -> GMorphism -> Json
gmorph :: HetcatsOpts -> GlobalAnnos -> GMorphism -> Json
gmorph opts :: HetcatsOpts
opts ga :: GlobalAnnos
ga gm :: GMorphism
gm@(GMorphism cid :: cid
cid (ExtSign ssig :: sign1
ssig _) _ tmor :: morphism2
tmor _) =
  case cid -> sign1 -> Result (sign2, [Named sentence2])
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid -> sign1 -> Result (sign2, [Named sentence2])
map_sign cid
cid sign1
ssig of
    Result _ mr :: Maybe (sign2, [Named sentence2])
mr -> case Maybe (sign2, [Named sentence2])
mr of
      Nothing -> String -> Json
forall a. HasCallStack => String -> a
error (String -> Json) -> String -> Json
forall a b. (a -> b) -> a -> b
$ "Static.ToXml.gmorph: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ GlobalAnnos -> GMorphism -> String -> String
forall a. Pretty a => GlobalAnnos -> a -> String -> String
showGlobalDoc GlobalAnnos
ga GMorphism
gm ""
      Just (tsig :: sign2
tsig, tsens :: [Named sentence2]
tsens) -> let
        tid :: lid2
tid = cid -> lid2
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid -> lid2
targetLogic cid
cid
        sl :: [(symbol2, symbol2)]
sl = Map symbol2 symbol2 -> [(symbol2, symbol2)]
forall k a. Map k a -> [(k, a)]
Map.toList (Map symbol2 symbol2 -> [(symbol2, symbol2)])
-> (Map symbol2 symbol2 -> Map symbol2 symbol2)
-> Map symbol2 symbol2
-> [(symbol2, symbol2)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (symbol2 -> symbol2 -> Bool)
-> Map symbol2 symbol2 -> Map symbol2 symbol2
forall k a. (k -> a -> Bool) -> Map k a -> Map k a
Map.filterWithKey symbol2 -> symbol2 -> Bool
forall a. Eq a => a -> a -> Bool
(/=) (Map symbol2 symbol2 -> [(symbol2, symbol2)])
-> Map symbol2 symbol2 -> [(symbol2, symbol2)]
forall a b. (a -> b) -> a -> b
$ lid2 -> morphism2 -> Map symbol2 symbol2
forall lid sentence sign morphism symbol.
Sentences lid sentence sign morphism symbol =>
lid -> morphism -> EndoMap symbol
symmap_of lid2
tid morphism2
tmor
        in [JPair] -> Json
mkJObj
        ([JPair] -> Json) -> [JPair] -> Json
forall a b. (a -> b) -> a -> b
$ String -> JPair
mkNameJPair (cid -> String
forall lid. Language lid => lid -> String
language_name cid
cid)
        JPair -> [JPair] -> [JPair]
forall a. a -> [a] -> [a]
: [("ComorphismAxioms", [Json] -> Json
mkJArr
            ([Json] -> Json) -> [Json] -> Json
forall a b. (a -> b) -> a -> b
$ (Named sentence2 -> Json) -> [Named sentence2] -> [Json]
forall a b. (a -> b) -> [a] -> [b]
map (HetcatsOpts
-> lid2
-> GlobalAnnos
-> Maybe Bool
-> sign2
-> Named sentence2
-> Json
forall sentence lid sign morphism symbol.
(GetRange sentence, Pretty sentence,
 Sentences lid sentence sign morphism symbol) =>
HetcatsOpts
-> lid
-> GlobalAnnos
-> Maybe Bool
-> sign
-> Named sentence
-> Json
showSen HetcatsOpts
opts (cid -> lid2
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid -> lid2
targetLogic cid
cid) GlobalAnnos
ga Maybe Bool
forall a. Maybe a
Nothing sign2
tsig) [Named sentence2]
tsens)
          | Bool -> Bool
not (HetcatsOpts -> Bool
fullTheories HetcatsOpts
opts) Bool -> Bool -> Bool
&& Bool -> Bool
not ([Named sentence2] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Named sentence2]
tsens) ]
        [JPair] -> [JPair] -> [JPair]
forall a. [a] -> [a] -> [a]
++ [("Map", [Json] -> Json
mkJArr ([Json] -> Json) -> [Json] -> Json
forall a b. (a -> b) -> a -> b
$
             ((symbol2, symbol2) -> Json) -> [(symbol2, symbol2)] -> [Json]
forall a b. (a -> b) -> [a] -> [b]
map (\ (s :: symbol2
s, t :: symbol2
t) -> [JPair] -> Json
mkJObj
             [("map", lid2 -> symbol2 -> Json
forall lid sentence sign morphism symbol.
Sentences lid sentence sign morphism symbol =>
lid -> symbol -> Json
showSym lid2
tid symbol2
s), ("to", lid2 -> symbol2 -> Json
forall lid sentence sign morphism symbol.
Sentences lid sentence sign morphism symbol =>
lid -> symbol -> Json
showSym lid2
tid symbol2
t)]) [(symbol2, symbol2)]
sl)
           | Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ [(symbol2, symbol2)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(symbol2, symbol2)]
sl]

prettySymbol :: (GetRange a, Pretty a) => GlobalAnnos -> a -> [JPair]
prettySymbol :: GlobalAnnos -> a -> [JPair]
prettySymbol = String -> GlobalAnnos -> a -> [JPair]
forall a.
(GetRange a, Pretty a) =>
String -> GlobalAnnos -> a -> [JPair]
rangedToJson "Symbol"

lnode :: HetcatsOpts -> GlobalAnnos -> LibEnv -> LNode DGNodeLab -> Json
lnode :: HetcatsOpts -> GlobalAnnos -> LibEnv -> LNode DGNodeLab -> Json
lnode opts :: HetcatsOpts
opts ga :: GlobalAnnos
ga lenv :: LibEnv
lenv (nodeId :: Int
nodeId, lbl :: DGNodeLab
lbl) =
  let nm :: NodeName
nm = DGNodeLab -> NodeName
dgn_name DGNodeLab
lbl
      (spn :: String
spn, xp :: String
xp) = case [XPathPart] -> [XPathPart]
forall a. [a] -> [a]
reverse ([XPathPart] -> [XPathPart]) -> [XPathPart] -> [XPathPart]
forall a b. (a -> b) -> a -> b
$ NodeName -> [XPathPart]
xpath NodeName
nm of
          ElemName s :: String
s : t :: [XPathPart]
t -> (String
s, [XPathPart] -> String
showXPath [XPathPart]
t)
          l :: [XPathPart]
l -> ("?", [XPathPart] -> String
showXPath [XPathPart]
l)
  in [JPair] -> Json
mkJObj
  ([JPair] -> Json) -> [JPair] -> Json
forall a b. (a -> b) -> a -> b
$ String -> JPair
mkNameJPair (NodeName -> String
showName NodeName
nm)
    JPair -> [JPair] -> [JPair]
forall a. a -> [a] -> [a]
: Range -> [JPair]
rangeToJPair (NodeName -> Range
srcRange NodeName
nm)
    [JPair] -> [JPair] -> [JPair]
forall a. [a] -> [a] -> [a]
++ [("id", Int -> Json
forall b. Real b => b -> Json
mkJNum Int
nodeId)]
    [JPair] -> [JPair] -> [JPair]
forall a. [a] -> [a] -> [a]
++ [("reference", Bool -> Json
mkJBool (Bool -> Json) -> Bool -> Json
forall a b. (a -> b) -> a -> b
$ DGNodeLab -> Bool
isDGRef DGNodeLab
lbl)]
    [JPair] -> [JPair] -> [JPair]
forall a. [a] -> [a] -> [a]
++ [("internal", Bool -> Json
mkJBool (Bool -> Json) -> Bool -> Json
forall a b. (a -> b) -> a -> b
$ NodeName -> Bool
isInternal NodeName
nm)]
    [JPair] -> [JPair] -> [JPair]
forall a. [a] -> [a] -> [a]
++ case G_theory -> G_sign
signOf (G_theory -> G_sign) -> G_theory -> G_sign
forall a b. (a -> b) -> a -> b
$ DGNodeLab -> G_theory
dgn_theory DGNodeLab
lbl of
        G_sign slid :: lid
slid _ _ -> String -> String -> JPair
mkJPair "logic" (lid -> String
forall a. Show a => a -> String
show lid
slid)
          JPair -> [JPair] -> [JPair]
forall a. a -> [a] -> [a]
: if Bool -> Bool
not (DGNodeLab -> Bool
isDGRef DGNodeLab
lbl) Bool -> Bool -> Bool
&& DGNodeLab -> DGOrigin
dgn_origin DGNodeLab
lbl DGOrigin -> DGOrigin -> Bool
forall a. Ord a => a -> a -> Bool
< DGOrigin
DGProof then
             [String -> String -> JPair
mkJPair "refname" String
spn, String -> String -> JPair
mkJPair "relxpath" String
xp ]
            else []
    [JPair] -> [JPair] -> [JPair]
forall a. [a] -> [a] -> [a]
++ case DGNodeLab -> DGNodeInfo
nodeInfo DGNodeLab
lbl of
          DGRef li :: LibName
li rf :: Int
rf ->
            [ ("Reference", [JPair] -> Json
mkJObj
              [ String -> String -> JPair
mkJPair "library" (String -> JPair) -> String -> JPair
forall a b. (a -> b) -> a -> b
$ IRI -> String
forall a. Show a => a -> String
show (IRI -> String) -> IRI -> String
forall a b. (a -> b) -> a -> b
$ Bool -> IRI -> IRI
setAngles Bool
False (IRI -> IRI) -> IRI -> IRI
forall a b. (a -> b) -> a -> b
$ LibName -> IRI
getLibId LibName
li
              , String -> String -> JPair
mkJPair "location" (String -> JPair) -> String -> JPair
forall a b. (a -> b) -> a -> b
$ LibName -> String
getFilePath LibName
li
              , String -> String -> JPair
mkJPair "node" (String -> JPair) -> String -> JPair
forall a b. (a -> b) -> a -> b
$ Int -> DGraph -> String
getNameOfNode Int
rf (DGraph -> String) -> DGraph -> String
forall a b. (a -> b) -> a -> b
$ LibName -> LibEnv -> DGraph
lookupDGraph LibName
li LibEnv
lenv ])]
          DGNode orig :: DGOrigin
orig cs :: ConsStatus
cs -> ConsStatus -> [JPair]
consStatus ConsStatus
cs [JPair] -> [JPair] -> [JPair]
forall a. [a] -> [a] -> [a]
++ case DGOrigin
orig of
                   DGBasicSpec _ (G_sign lid :: lid
lid (ExtSign dsig :: sign
dsig _) _) _ ->
                     let syms :: [symbol]
syms = lid -> sign -> [symbol]
forall lid sentence sign morphism symbol.
Sentences lid sentence sign morphism symbol =>
lid -> sign -> [symbol]
mostSymsOf lid
lid sign
dsig in
                         [ ("Declarations", lid -> [symbol] -> Json
forall lid sentence sign morphism symbol.
Sentences lid sentence sign morphism symbol =>
lid -> [symbol] -> Json
declarations lid
lid [symbol]
syms)
                           | Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ [symbol] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [symbol]
syms ]
                   DGRestriction _ hidSyms :: Set G_symbol
hidSyms ->
                     [ ("Hidden", [Json] -> Json
mkJArr
                       ([Json] -> Json) -> ([G_symbol] -> [Json]) -> [G_symbol] -> Json
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (G_symbol -> Json) -> [G_symbol] -> [Json]
forall a b. (a -> b) -> [a] -> [b]
map ([JPair] -> Json
mkJObj ([JPair] -> Json) -> (G_symbol -> [JPair]) -> G_symbol -> Json
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GlobalAnnos -> G_symbol -> [JPair]
forall a. (GetRange a, Pretty a) => GlobalAnnos -> a -> [JPair]
prettySymbol GlobalAnnos
ga)
                       ([G_symbol] -> Json) -> [G_symbol] -> Json
forall a b. (a -> b) -> a -> b
$ Set G_symbol -> [G_symbol]
forall a. Set a -> [a]
Set.toList Set G_symbol
hidSyms) ]
                   _ -> []
      [JPair] -> [JPair] -> [JPair]
forall a. [a] -> [a] -> [a]
++ case DGNodeLab -> G_theory
dgn_theory DGNodeLab
lbl of
        G_theory lid :: lid
lid _ extSig :: ExtSign sign symbol
extSig@(ExtSign sig :: sign
sig _) _ thsens :: ThSens sentence (AnyComorphism, BasicProof)
thsens _ -> let
          (axs :: ThSens sentence (AnyComorphism, BasicProof)
axs, thms :: ThSens sentence (AnyComorphism, BasicProof)
thms) = (SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)) -> Bool)
-> ThSens sentence (AnyComorphism, BasicProof)
-> (ThSens sentence (AnyComorphism, BasicProof),
    ThSens sentence (AnyComorphism, BasicProof))
forall k a.
Ord k =>
(a -> Bool) -> OMap k a -> (OMap k a, OMap k a)
OMap.partition SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)) -> Bool
forall s a. SenAttr s a -> Bool
isAxiom ThSens sentence (AnyComorphism, BasicProof)
thsens
          nAxs :: [Named sentence]
nAxs = ThSens sentence (AnyComorphism, BasicProof) -> [Named sentence]
forall a b. ThSens a b -> [Named a]
toNamedList ThSens sentence (AnyComorphism, BasicProof)
axs
          nThms :: [(String,
  SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)))]
nThms = ThSens sentence (AnyComorphism, BasicProof)
-> [(String,
     SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)))]
forall k a. Ord k => OMap k a -> [(k, a)]
OMap.toList ThSens sentence (AnyComorphism, BasicProof)
thms
          in
          [("Symbols", lid -> ExtSign sign symbol -> Json
forall lid sentence sign morphism symbol.
Sentences lid sentence sign morphism symbol =>
lid -> ExtSign sign symbol -> Json
symbols lid
lid ExtSign sign symbol
extSig)
          | HetcatsOpts -> Bool
fullSign HetcatsOpts
opts ]
          [JPair] -> [JPair] -> [JPair]
forall a. [a] -> [a] -> [a]
++ [("Axioms", [Json] -> Json
mkJArr
             ([Json] -> Json) -> [Json] -> Json
forall a b. (a -> b) -> a -> b
$ (Named sentence -> Json) -> [Named sentence] -> [Json]
forall a b. (a -> b) -> [a] -> [b]
map (HetcatsOpts
-> lid
-> GlobalAnnos
-> Maybe Bool
-> sign
-> Named sentence
-> Json
forall sentence lid sign morphism symbol.
(GetRange sentence, Pretty sentence,
 Sentences lid sentence sign morphism symbol) =>
HetcatsOpts
-> lid
-> GlobalAnnos
-> Maybe Bool
-> sign
-> Named sentence
-> Json
showSen HetcatsOpts
opts lid
lid GlobalAnnos
ga Maybe Bool
forall a. Maybe a
Nothing sign
sig) [Named sentence]
nAxs) | Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ [Named sentence] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Named sentence]
nAxs ]
          [JPair] -> [JPair] -> [JPair]
forall a. [a] -> [a] -> [a]
++ [("Theorems", [Json] -> Json
mkJArr
             ([Json] -> Json) -> [Json] -> Json
forall a b. (a -> b) -> a -> b
$ ((String, SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)))
 -> Json)
-> [(String,
     SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)))]
-> [Json]
forall a b. (a -> b) -> [a] -> [b]
map (\ (s :: String
s, t :: SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))
t) -> HetcatsOpts
-> lid
-> GlobalAnnos
-> Maybe Bool
-> sign
-> Named sentence
-> Json
forall sentence lid sign morphism symbol.
(GetRange sentence, Pretty sentence,
 Sentences lid sentence sign morphism symbol) =>
HetcatsOpts
-> lid
-> GlobalAnnos
-> Maybe Bool
-> sign
-> Named sentence
-> Json
showSen HetcatsOpts
opts lid
lid GlobalAnnos
ga
                         (Bool -> Maybe Bool
forall a. a -> Maybe a
Just (Bool -> Maybe Bool) -> Bool -> Maybe Bool
forall a b. (a -> b) -> a -> b
$ SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)) -> Bool
forall a. SenStatus a (AnyComorphism, BasicProof) -> Bool
isProvenSenStatus SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))
t) sign
sig (Named sentence -> Json) -> Named sentence -> Json
forall a b. (a -> b) -> a -> b
$ String
-> SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))
-> Named sentence
forall a b. String -> SenStatus a b -> Named a
toNamed String
s SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))
t)
                         [(String,
  SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)))]
nThms) | Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ [(String,
  SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)))]
-> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(String,
  SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)))]
nThms]
          [JPair] -> [JPair] -> [JPair]
forall a. [a] -> [a] -> [a]
++ if HetcatsOpts -> Bool
fullTheories HetcatsOpts
opts then case DGNodeLab -> Maybe G_theory
globalTheory DGNodeLab
lbl of
               Just (G_theory glid :: lid
glid _ _ _ allSens :: ThSens sentence (AnyComorphism, BasicProof)
allSens _) -> case
                   lid
-> lid
-> String
-> ThSens sentence (AnyComorphism, BasicProof)
-> Maybe (ThSens sentence (AnyComorphism, BasicProof))
forall lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2 (m :: * -> *) b.
(Logic
   lid1
   sublogics1
   basic_spec1
   sentence1
   symb_items1
   symb_map_items1
   sign1
   morphism1
   symbol1
   raw_symbol1
   proof_tree1,
 Logic
   lid2
   sublogics2
   basic_spec2
   sentence2
   symb_items2
   symb_map_items2
   sign2
   morphism2
   symbol2
   raw_symbol2
   proof_tree2,
 MonadFail m, Typeable b) =>
lid1
-> lid2 -> String -> ThSens sentence1 b -> m (ThSens sentence2 b)
coerceThSens lid
glid lid
lid "xml-lnode" ThSens sentence (AnyComorphism, BasicProof)
allSens of
                 Just gsens :: ThSens sentence (AnyComorphism, BasicProof)
gsens -> let
                   nSens :: [Named sentence]
nSens = ThSens sentence (AnyComorphism, BasicProof) -> [Named sentence]
forall a b. ThSens a b -> [Named a]
toNamedList
                     (ThSens sentence (AnyComorphism, BasicProof) -> [Named sentence])
-> ThSens sentence (AnyComorphism, BasicProof) -> [Named sentence]
forall a b. (a -> b) -> a -> b
$ (SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)) -> Bool)
-> ThSens sentence (AnyComorphism, BasicProof)
-> ThSens sentence (AnyComorphism, BasicProof)
forall k a. Ord k => (a -> Bool) -> OMap k a -> OMap k a
OMap.filter ((sentence -> [sentence] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` (SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))
 -> sentence)
-> [SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))]
-> [sentence]
forall a b. (a -> b) -> [a] -> [b]
map SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))
-> sentence
forall s a. SenAttr s a -> s
sentence
                                    (ThSens sentence (AnyComorphism, BasicProof)
-> [SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))]
forall k a. Ord k => OMap k a -> [a]
OMap.elems ThSens sentence (AnyComorphism, BasicProof)
thsens)) (sentence -> Bool)
-> (SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))
    -> sentence)
-> SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))
-> sentence
forall s a. SenAttr s a -> s
sentence) ThSens sentence (AnyComorphism, BasicProof)
gsens
                     in [("ImpAxioms", [Json] -> Json
mkJArr
                          ([Json] -> Json) -> [Json] -> Json
forall a b. (a -> b) -> a -> b
$ (Named sentence -> Json) -> [Named sentence] -> [Json]
forall a b. (a -> b) -> [a] -> [b]
map (HetcatsOpts
-> lid
-> GlobalAnnos
-> Maybe Bool
-> sign
-> Named sentence
-> Json
forall sentence lid sign morphism symbol.
(GetRange sentence, Pretty sentence,
 Sentences lid sentence sign morphism symbol) =>
HetcatsOpts
-> lid
-> GlobalAnnos
-> Maybe Bool
-> sign
-> Named sentence
-> Json
showSen HetcatsOpts
opts lid
lid GlobalAnnos
ga Maybe Bool
forall a. Maybe a
Nothing sign
sig) [Named sentence]
nSens)
                        | Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ [Named sentence] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Named sentence]
nSens ]
                 _ -> []
               _ -> []
             else []

-- | a status may be open, proven or outdated
mkStatusJPair :: String -> JPair
mkStatusJPair :: String -> JPair
mkStatusJPair = String -> String -> JPair
mkJPair "status"

mkProvenJPair :: Bool -> JPair
mkProvenJPair :: Bool -> JPair
mkProvenJPair b :: Bool
b = String -> JPair
mkStatusJPair (String -> JPair) -> String -> JPair
forall a b. (a -> b) -> a -> b
$ if Bool
b then "proven" else "open"

consStatus :: ConsStatus -> [JPair]
consStatus :: ConsStatus -> [JPair]
consStatus cs :: ConsStatus
cs = case ConsStatus -> Conservativity
getConsOfStatus ConsStatus
cs of
  None -> []
  cStat :: Conservativity
cStat -> [("ConsStatus", String -> Json
mkJStr (String -> Json) -> String -> Json
forall a b. (a -> b) -> a -> b
$ Conservativity -> String
forall a. Show a => a -> String
show Conservativity
cStat)]

ledge :: HetcatsOpts -> GlobalAnnos -> DGraph -> LEdge DGLinkLab -> Json
ledge :: HetcatsOpts -> GlobalAnnos -> DGraph -> LEdge DGLinkLab -> Json
ledge opts :: HetcatsOpts
opts ga :: GlobalAnnos
ga dg :: DGraph
dg (f :: Int
f, t :: Int
t, lbl :: DGLinkLab
lbl) = let
  typ :: DGLinkType
typ = DGLinkLab -> DGLinkType
dgl_type DGLinkLab
lbl
  mor :: Json
mor = HetcatsOpts -> GlobalAnnos -> GMorphism -> Json
gmorph HetcatsOpts
opts GlobalAnnos
ga (GMorphism -> Json) -> GMorphism -> Json
forall a b. (a -> b) -> a -> b
$ DGLinkLab -> GMorphism
dgl_morphism DGLinkLab
lbl
  mkMor :: Int -> [JPair]
mkMor n :: Int
n = [String -> String -> JPair
mkJPair "morphismsource" (String -> JPair) -> String -> JPair
forall a b. (a -> b) -> a -> b
$ Int -> DGraph -> String
getNameOfNode Int
n DGraph
dg]
  lnkSt :: [JPair]
lnkSt = case DGLinkType -> Maybe ThmLinkStatus
thmLinkStatus DGLinkType
typ of
         Nothing -> []
         Just tls :: ThmLinkStatus
tls -> case ThmLinkStatus
tls of
            LeftOpen -> []
            Proven r :: DGRule
r ls :: ProofBasis
ls -> DGRule -> [JPair]
dgrule DGRule
r
              [JPair] -> [JPair] -> [JPair]
forall a. [a] -> [a] -> [a]
++ let bs :: [EdgeId]
bs = Set EdgeId -> [EdgeId]
forall a. Set a -> [a]
Set.toList (Set EdgeId -> [EdgeId]) -> Set EdgeId -> [EdgeId]
forall a b. (a -> b) -> a -> b
$ ProofBasis -> Set EdgeId
proofBasis ProofBasis
ls in
                 [("ProofBasis", [Json] -> Json
mkJArr
                   ([Json] -> Json) -> [Json] -> Json
forall a b. (a -> b) -> a -> b
$ (EdgeId -> Json) -> [EdgeId] -> [Json]
forall a b. (a -> b) -> [a] -> [b]
map (Int -> Json
forall b. Real b => b -> Json
mkJNum (Int -> Json) -> (EdgeId -> Int) -> EdgeId -> Json
forall b c a. (b -> c) -> (a -> b) -> a -> c
. EdgeId -> Int
getEdgeNum) [EdgeId]
bs) | Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ [EdgeId] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [EdgeId]
bs]
  in [JPair] -> Json
mkJObj
  ([JPair] -> Json) -> [JPair] -> Json
forall a b. (a -> b) -> a -> b
$ [ String -> String -> JPair
mkJPair "source" (String -> JPair) -> String -> JPair
forall a b. (a -> b) -> a -> b
$ Int -> DGraph -> String
getNameOfNode Int
f DGraph
dg
  , String -> String -> JPair
mkJPair "target" (String -> JPair) -> String -> JPair
forall a b. (a -> b) -> a -> b
$ Int -> DGraph -> String
getNameOfNode Int
t DGraph
dg
  , ("linkid", Int -> Json
forall b. Real b => b -> Json
mkJNum (Int -> Json) -> (EdgeId -> Int) -> EdgeId -> Json
forall b c a. (b -> c) -> (a -> b) -> a -> c
. EdgeId -> Int
getEdgeNum (EdgeId -> Json) -> EdgeId -> Json
forall a b. (a -> b) -> a -> b
$ DGLinkLab -> EdgeId
dgl_id DGLinkLab
lbl)
  , ("id_source", Int -> Json
forall b. Real b => b -> Json
mkJNum Int
f)
  , ("id_target", Int -> Json
forall b. Real b => b -> Json
mkJNum Int
t) ]
  [JPair] -> [JPair] -> [JPair]
forall a. [a] -> [a] -> [a]
++ case DGLinkLab -> DGLinkOrigin
dgl_origin DGLinkLab
lbl of
         DGLinkView i :: IRI
i _ ->
           [String -> JPair
mkNameJPair (String -> JPair) -> (IRI -> String) -> IRI -> JPair
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IRI -> String
iriToStringShortUnsecure (IRI -> JPair) -> IRI -> JPair
forall a b. (a -> b) -> a -> b
$ Bool -> IRI -> IRI
setAngles Bool
False IRI
i]
         _ -> []
  [JPair] -> [JPair] -> [JPair]
forall a. [a] -> [a] -> [a]
++ String -> String -> JPair
mkJPair "Type" (DGLinkLab -> String
getDGLinkType DGLinkLab
lbl) JPair -> [JPair] -> [JPair]
forall a. a -> [a] -> [a]
: [JPair]
lnkSt
    [JPair] -> [JPair] -> [JPair]
forall a. [a] -> [a] -> [a]
++ ConsStatus -> [JPair]
consStatus (DGLinkType -> ConsStatus
getLinkConsStatus DGLinkType
typ)
    [JPair] -> [JPair] -> [JPair]
forall a. [a] -> [a] -> [a]
++ case DGLinkType
typ of
         HidingFreeOrCofreeThm _ n :: Int
n _ _ -> Int -> [JPair]
mkMor Int
n
         FreeOrCofreeDefLink _ (JustNode ns :: NodeSig
ns) -> Int -> [JPair]
mkMor (Int -> [JPair]) -> Int -> [JPair]
forall a b. (a -> b) -> a -> b
$ NodeSig -> Int
getNode NodeSig
ns
         _ -> []
    [JPair] -> [JPair] -> [JPair]
forall a. [a] -> [a] -> [a]
++ [("GMorphism", Json
mor)]

dgrule :: DGRule -> [JPair]
dgrule :: DGRule -> [JPair]
dgrule r :: DGRule
r =
  String -> String -> JPair
mkJPair "Rule" (DGRule -> String
dgRuleHeader DGRule
r)
  JPair -> [JPair] -> [JPair]
forall a. a -> [a] -> [a]
: case DGRule
r of
      DGRuleLocalInference m :: [(String, String)]
m -> [("MovedTheorems", [Json] -> Json
mkJArr
        ([Json] -> Json) -> [Json] -> Json
forall a b. (a -> b) -> a -> b
$ ((String, String) -> Json) -> [(String, String)] -> [Json]
forall a b. (a -> b) -> [a] -> [b]
map (\ (s :: String
s, t :: String
t) -> [JPair] -> Json
mkJObj [String -> JPair
mkNameJPair String
s, String -> String -> JPair
mkJPair "renamedTo" String
t]) [(String, String)]
m)]
      Composition es :: [EdgeId]
es ->
        [("Composition", [Json] -> Json
mkJArr ([Json] -> Json) -> [Json] -> Json
forall a b. (a -> b) -> a -> b
$ (EdgeId -> Json) -> [EdgeId] -> [Json]
forall a b. (a -> b) -> [a] -> [b]
map (Int -> Json
forall b. Real b => b -> Json
mkJNum (Int -> Json) -> (EdgeId -> Int) -> EdgeId -> Json
forall b c a. (b -> c) -> (a -> b) -> a -> c
. EdgeId -> Int
getEdgeNum) [EdgeId]
es)]
      DGRuleWithEdge _ e :: EdgeId
e -> [("RuleTarget", Int -> Json
forall b. Real b => b -> Json
mkJNum (Int -> Json) -> Int -> Json
forall a b. (a -> b) -> a -> b
$ EdgeId -> Int
getEdgeNum EdgeId
e)]
      _ -> []

-- | collects all symbols from dg and displays them as json
dgSymbols :: HetcatsOpts -> DGraph -> Json
dgSymbols :: HetcatsOpts -> DGraph -> Json
dgSymbols opts :: HetcatsOpts
opts dg :: DGraph
dg = let ga :: GlobalAnnos
ga = DGraph -> GlobalAnnos
globalAnnos DGraph
dg in String -> Json -> Json
tagJson "Ontologies"
  (Json -> Json) -> Json -> Json
forall a b. (a -> b) -> a -> b
$ [Json] -> Json
mkJArr ([Json] -> Json) -> [Json] -> Json
forall a b. (a -> b) -> a -> b
$ (LNode DGNodeLab -> Json) -> [LNode DGNodeLab] -> [Json]
forall a b. (a -> b) -> [a] -> [b]
map (\ (i :: Int
i, lbl :: DGNodeLab
lbl) -> let ins :: [String]
ins = DGraph -> Int -> [String]
getImportNames DGraph
dg Int
i in
    HetcatsOpts -> [String] -> GlobalAnnos -> DGNodeLab -> Json
showSymbols HetcatsOpts
opts [String]
ins GlobalAnnos
ga DGNodeLab
lbl) ([LNode DGNodeLab] -> [Json]) -> [LNode DGNodeLab] -> [Json]
forall a b. (a -> b) -> a -> b
$ DGraph -> [LNode DGNodeLab]
labNodesDG DGraph
dg

showSymbols :: HetcatsOpts -> [String] -> GlobalAnnos -> DGNodeLab -> Json
showSymbols :: HetcatsOpts -> [String] -> GlobalAnnos -> DGNodeLab -> Json
showSymbols opts :: HetcatsOpts
opts ins :: [String]
ins ga :: GlobalAnnos
ga lbl :: DGNodeLab
lbl = HetcatsOpts
-> [String] -> String -> GlobalAnnos -> G_theory -> Json
showSymbolsTh HetcatsOpts
opts [String]
ins (DGNodeLab -> String
getDGNodeName DGNodeLab
lbl) GlobalAnnos
ga
  (G_theory -> Json) -> G_theory -> Json
forall a b. (a -> b) -> a -> b
$ DGNodeLab -> G_theory
dgn_theory DGNodeLab
lbl

showSymbolsTh :: HetcatsOpts -> [String] -> String -> GlobalAnnos -> G_theory -> Json
showSymbolsTh :: HetcatsOpts
-> [String] -> String -> GlobalAnnos -> G_theory -> Json
showSymbolsTh opts :: HetcatsOpts
opts ins :: [String]
ins name :: String
name ga :: GlobalAnnos
ga th :: G_theory
th = case G_theory
th of
  G_theory lid :: lid
lid _ (ExtSign sig :: sign
sig _) _ sens :: ThSens sentence (AnyComorphism, BasicProof)
sens _ -> [JPair] -> Json
mkJObj
     [ String -> String -> JPair
mkJPair "logic" (String -> JPair) -> String -> JPair
forall a b. (a -> b) -> a -> b
$ lid -> String
forall lid. Language lid => lid -> String
language_name lid
lid
     , String -> JPair
mkNameJPair String
name
     , ("Ontology", [JPair] -> Json
mkJObj
       [ ("Symbols", [Json] -> Json
mkJArr ([Json] -> Json) -> ([symbol] -> [Json]) -> [symbol] -> Json
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (symbol -> Json) -> [symbol] -> [Json]
forall a b. (a -> b) -> [a] -> [b]
map (lid -> symbol -> Json
forall lid sentence sign morphism symbol.
Sentences lid sentence sign morphism symbol =>
lid -> symbol -> Json
showSym lid
lid) ([symbol] -> Json) -> [symbol] -> Json
forall a b. (a -> b) -> a -> b
$ lid -> sign -> [symbol]
forall lid sentence sign morphism symbol.
Sentences lid sentence sign morphism symbol =>
lid -> sign -> [symbol]
symlist_of lid
lid sign
sig)
       , ("Axioms", [Json] -> Json
mkJArr ([Json] -> Json)
-> ([Named sentence] -> [Json]) -> [Named sentence] -> Json
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Named sentence -> Json) -> [Named sentence] -> [Json]
forall a b. (a -> b) -> [a] -> [b]
map (HetcatsOpts
-> lid
-> GlobalAnnos
-> Maybe Bool
-> sign
-> Named sentence
-> Json
forall sentence lid sign morphism symbol.
(GetRange sentence, Pretty sentence,
 Sentences lid sentence sign morphism symbol) =>
HetcatsOpts
-> lid
-> GlobalAnnos
-> Maybe Bool
-> sign
-> Named sentence
-> Json
showSen HetcatsOpts
opts lid
lid GlobalAnnos
ga Maybe Bool
forall a. Maybe a
Nothing sign
sig)
         ([Named sentence] -> Json) -> [Named sentence] -> Json
forall a b. (a -> b) -> a -> b
$ ThSens sentence (AnyComorphism, BasicProof) -> [Named sentence]
forall a b. ThSens a b -> [Named a]
toNamedList ThSens sentence (AnyComorphism, BasicProof)
sens)
       , ("Import", [Json] -> Json
mkJArr ([Json] -> Json) -> [Json] -> Json
forall a b. (a -> b) -> a -> b
$ (String -> Json) -> [String] -> [Json]
forall a b. (a -> b) -> [a] -> [b]
map String -> Json
mkJStr [String]
ins) ])]

showSen :: ( GetRange sentence, Pretty sentence
           , Sentences lid sentence sign morphism symbol) =>
   HetcatsOpts -> lid -> GlobalAnnos -> Maybe Bool -> sign -> Named sentence -> Json
showSen :: HetcatsOpts
-> lid
-> GlobalAnnos
-> Maybe Bool
-> sign
-> Named sentence
-> Json
showSen opts :: HetcatsOpts
opts lid :: lid
lid ga :: GlobalAnnos
ga mt :: Maybe Bool
mt sig :: sign
sig ns :: Named sentence
ns = let s :: sentence
s = Named sentence -> sentence
forall s a. SenAttr s a -> s
sentence Named sentence
ns in [JPair] -> Json
mkJObj
    ([JPair] -> Json) -> [JPair] -> Json
forall a b. (a -> b) -> a -> b
$ case Maybe Bool
mt of
       Nothing -> []
       Just b :: Bool
b -> [Bool -> JPair
mkProvenJPair Bool
b]
     [JPair] -> [JPair] -> [JPair]
forall a. [a] -> [a] -> [a]
++ String -> JPair
mkNameJPair (Named sentence -> String
forall s a. SenAttr s a -> a
senAttr Named sentence
ns) JPair -> [JPair] -> [JPair]
forall a. a -> [a] -> [a]
: Range -> [JPair]
rangeToJPair (sentence -> Range
forall a. GetRange a => a -> Range
getRangeSpan sentence
s)
     [JPair] -> [JPair] -> [JPair]
forall a. [a] -> [a] -> [a]
++ case Named sentence -> Maybe String
forall s a. SenAttr s a -> Maybe String
priority Named sentence
ns of
          Just p :: String
p -> [String -> JPair
mkPriorityJPair String
p]
          _ -> []
     [JPair] -> [JPair] -> [JPair]
forall a. [a] -> [a] -> [a]
++ String -> String -> JPair
mkJPair (if Maybe Bool -> Bool
forall a. Maybe a -> Bool
isJust Maybe Bool
mt then "Theorem" else "Axiom")
          (Doc -> String
forall a. Show a => a -> String
show (Doc -> String) -> (sentence -> Doc) -> sentence -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GlobalAnnos -> Doc -> Doc
useGlobalAnnos GlobalAnnos
ga (Doc -> Doc) -> (sentence -> Doc) -> sentence -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. lid -> Named sentence -> Doc
forall lid sentence sign morphism symbol.
Sentences lid sentence sign morphism symbol =>
lid -> Named sentence -> Doc
print_named lid
lid
                            (Named sentence -> Doc)
-> (sentence -> Named sentence) -> sentence -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> sentence -> Named sentence
forall a s. a -> s -> SenAttr s a
makeNamed "" (sentence -> String) -> sentence -> String
forall a b. (a -> b) -> a -> b
$ lid -> sign -> sentence -> sentence
forall lid sentence sign morphism symbol.
Sentences lid sentence sign morphism symbol =>
lid -> sign -> sentence -> sentence
simplify_sen lid
lid sign
sig sentence
s)
          JPair -> [JPair] -> [JPair]
forall a. a -> [a] -> [a]
: (let syms :: [symbol]
syms = lid -> sign -> sentence -> [symbol]
forall lid sentence sign morphism symbol.
Sentences lid sentence sign morphism symbol =>
lid -> sign -> sentence -> [symbol]
symsOfSen lid
lid sign
sig sentence
s in
              [("SenSymbols", [Json] -> Json
mkJArr ([Json] -> Json) -> [Json] -> Json
forall a b. (a -> b) -> a -> b
$ (symbol -> Json) -> [symbol] -> [Json]
forall a b. (a -> b) -> [a] -> [b]
map (lid -> symbol -> Json
forall lid sentence sign morphism symbol.
Sentences lid sentence sign morphism symbol =>
lid -> symbol -> Json
showSym lid
lid) [symbol]
syms)
               | Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ [symbol] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [symbol]
syms])
          [JPair] -> [JPair] -> [JPair]
forall a. [a] -> [a] -> [a]
++ case Named sentence -> String
forall s a. SenAttr s a -> String
senMark Named sentence
ns of
               "" -> []
               m :: String
m -> [String -> String -> JPair
mkJPair "ComorphismOrigin" String
m]
          [JPair] -> [JPair] -> [JPair]
forall a. [a] -> [a] -> [a]
++ if HetcatsOpts -> Bool
printAST HetcatsOpts
opts
             then [("AST", sentence -> Json
forall a. ToJson a => a -> Json
asJson sentence
s)]
             else []

declarations :: Sentences lid sentence sign morphism symbol
             => lid -> [symbol] -> Json
declarations :: lid -> [symbol] -> Json
declarations lid :: lid
lid syms :: [symbol]
syms = [Json] -> Json
mkJArr ([Json] -> Json) -> [Json] -> Json
forall a b. (a -> b) -> a -> b
$ (symbol -> Json) -> [symbol] -> [Json]
forall a b. (a -> b) -> [a] -> [b]
map (lid -> symbol -> Json
forall lid sentence sign morphism symbol.
Sentences lid sentence sign morphism symbol =>
lid -> symbol -> Json
showSym lid
lid) [symbol]
syms

symbols :: Sentences lid sentence sign morphism symbol
        => lid -> ExtSign sign symbol -> Json
symbols :: lid -> ExtSign sign symbol -> Json
symbols lid :: lid
lid (ExtSign sig :: sign
sig _) = [Json] -> Json
mkJArr ([Json] -> Json) -> ([symbol] -> [Json]) -> [symbol] -> Json
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (symbol -> Json) -> [symbol] -> [Json]
forall a b. (a -> b) -> [a] -> [b]
map (lid -> symbol -> Json
forall lid sentence sign morphism symbol.
Sentences lid sentence sign morphism symbol =>
lid -> symbol -> Json
showSym lid
lid) ([symbol] -> Json) -> [symbol] -> Json
forall a b. (a -> b) -> a -> b
$ lid -> sign -> [symbol]
forall lid sentence sign morphism symbol.
Sentences lid sentence sign morphism symbol =>
lid -> sign -> [symbol]
symlist_of lid
lid sign
sig

showSym :: Sentences lid sentence sign morphism symbol => lid -> symbol -> Json
showSym :: lid -> symbol -> Json
showSym lid :: lid
lid s :: symbol
s = [JPair] -> Json
mkJObj
  ([JPair] -> Json) -> [JPair] -> Json
forall a b. (a -> b) -> a -> b
$ [ String -> String -> JPair
mkJPair "kind" (String -> JPair) -> String -> JPair
forall a b. (a -> b) -> a -> b
$ lid -> symbol -> String
forall lid sentence sign morphism symbol.
Sentences lid sentence sign morphism symbol =>
lid -> symbol -> String
symKind lid
lid symbol
s
    , String -> JPair
mkNameJPair (String -> JPair) -> (Id -> String) -> Id -> JPair
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Id -> String
forall a. Show a => a -> String
show (Id -> JPair) -> Id -> JPair
forall a b. (a -> b) -> a -> b
$ lid -> symbol -> Id
forall lid sentence sign morphism symbol.
Sentences lid sentence sign morphism symbol =>
lid -> symbol -> Id
sym_name lid
lid symbol
s
    , String -> String -> JPair
mkJPair "iri" (String -> JPair) -> String -> JPair
forall a b. (a -> b) -> a -> b
$ lid -> symbol -> String
forall lid sentence sign morphism symbol.
Sentences lid sentence sign morphism symbol =>
lid -> symbol -> String
fullSymName lid
lid symbol
s ]
    [JPair] -> [JPair] -> [JPair]
forall a. [a] -> [a] -> [a]
++ GlobalAnnos -> symbol -> [JPair]
forall a. (GetRange a, Pretty a) => GlobalAnnos -> a -> [JPair]
prettySymbol GlobalAnnos
emptyGlobalAnnos symbol
s