{- |
Module      :  ./Logic/LGToJson.hs
Description :  export logic graph information as Json
Copyright   :  (c) Christian Maeder DFKI GmbH 2013
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  Christian.Maeder@dfki.de
Stability   :  provisional
Portability :  non-portable (via imports)

export logic graph information as Json
-}

module Logic.LGToJson where

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

import Control.Monad

import qualified Data.Map as Map
import Data.Maybe

import Common.Consistency
import Common.Json

usableProvers :: LogicGraph -> IO Json
usableProvers :: LogicGraph -> IO Json
usableProvers lg :: LogicGraph
lg = do
  [[Json]]
ps <- (AnyLogic -> IO [Json]) -> [AnyLogic] -> IO [[Json]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM AnyLogic -> IO [Json]
proversOfLogic ([AnyLogic] -> IO [[Json]])
-> (Map String AnyLogic -> [AnyLogic])
-> Map String AnyLogic
-> IO [[Json]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map String AnyLogic -> [AnyLogic]
forall k a. Map k a -> [a]
Map.elems (Map String AnyLogic -> IO [[Json]])
-> Map String AnyLogic -> IO [[Json]]
forall a b. (a -> b) -> a -> b
$ LogicGraph -> Map String AnyLogic
logics LogicGraph
lg
  Json -> IO Json
forall (m :: * -> *) a. Monad m => a -> m a
return (Json -> IO Json) -> Json -> IO Json
forall a b. (a -> b) -> a -> b
$ [JPair] -> Json
mkJObj [("provers", [Json] -> Json
mkJArr ([Json] -> Json) -> [Json] -> Json
forall a b. (a -> b) -> a -> b
$ [[Json]] -> [Json]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[Json]]
ps)]

proversOfLogic :: AnyLogic -> IO [Json]
proversOfLogic :: AnyLogic -> IO [Json]
proversOfLogic (Logic lid :: lid
lid) = do
  [ProverTemplate
   (Theory sign sentence proof_tree)
   sentence
   morphism
   sublogics
   proof_tree]
bps <- (ProverTemplate
   (Theory sign sentence proof_tree)
   sentence
   morphism
   sublogics
   proof_tree
 -> IO Bool)
-> [ProverTemplate
      (Theory sign sentence proof_tree)
      sentence
      morphism
      sublogics
      proof_tree]
-> IO
     [ProverTemplate
        (Theory sign sentence proof_tree)
        sentence
        morphism
        sublogics
        proof_tree]
forall (m :: * -> *) a.
Applicative m =>
(a -> m Bool) -> [a] -> m [a]
filterM ((Maybe String -> Bool) -> IO (Maybe String) -> IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Maybe String -> Bool
forall a. Maybe a -> Bool
isNothing (IO (Maybe String) -> IO Bool)
-> (ProverTemplate
      (Theory sign sentence proof_tree)
      sentence
      morphism
      sublogics
      proof_tree
    -> IO (Maybe String))
-> ProverTemplate
     (Theory sign sentence proof_tree)
     sentence
     morphism
     sublogics
     proof_tree
-> IO Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ProverTemplate
  (Theory sign sentence proof_tree)
  sentence
  morphism
  sublogics
  proof_tree
-> IO (Maybe String)
forall theory sentence morphism sublogics proof_tree.
ProverTemplate theory sentence morphism sublogics proof_tree
-> IO (Maybe String)
proverUsable) ([ProverTemplate
    (Theory sign sentence proof_tree)
    sentence
    morphism
    sublogics
    proof_tree]
 -> IO
      [ProverTemplate
         (Theory sign sentence proof_tree)
         sentence
         morphism
         sublogics
         proof_tree])
-> [ProverTemplate
      (Theory sign sentence proof_tree)
      sentence
      morphism
      sublogics
      proof_tree]
-> IO
     [ProverTemplate
        (Theory sign sentence proof_tree)
        sentence
        morphism
        sublogics
        proof_tree]
forall a b. (a -> b) -> a -> b
$ lid
-> [ProverTemplate
      (Theory sign sentence proof_tree)
      sentence
      morphism
      sublogics
      proof_tree]
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> [Prover sign sentence morphism sublogics proof_tree]
provers lid
lid
  [Json] -> IO [Json]
forall (m :: * -> *) a. Monad m => a -> m a
return ([Json] -> IO [Json]) -> [Json] -> IO [Json]
forall a b. (a -> b) -> a -> b
$ (ProverTemplate
   (Theory sign sentence proof_tree)
   sentence
   morphism
   sublogics
   proof_tree
 -> Json)
-> [ProverTemplate
      (Theory sign sentence proof_tree)
      sentence
      morphism
      sublogics
      proof_tree]
-> [Json]
forall a b. (a -> b) -> [a] -> [b]
map (\ p :: ProverTemplate
  (Theory sign sentence proof_tree)
  sentence
  morphism
  sublogics
  proof_tree
p ->
      [JPair] -> Json
mkJObj [ String -> JPair
mkNameJPair (String -> JPair) -> String -> JPair
forall a b. (a -> b) -> a -> b
$ ProverTemplate
  (Theory sign sentence proof_tree)
  sentence
  morphism
  sublogics
  proof_tree
-> String
forall theory sentence morphism sublogics proof_tree.
ProverTemplate theory sentence morphism sublogics proof_tree
-> String
proverName ProverTemplate
  (Theory sign sentence proof_tree)
  sentence
  morphism
  sublogics
  proof_tree
p
             , 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 ]) [ProverTemplate
   (Theory sign sentence proof_tree)
   sentence
   morphism
   sublogics
   proof_tree]
bps

lGToJson :: LogicGraph -> IO Json
lGToJson :: LogicGraph -> IO Json
lGToJson lg :: LogicGraph
lg = do
  let cs :: [AnyComorphism]
cs = Map String AnyComorphism -> [AnyComorphism]
forall k a. Map k a -> [a]
Map.elems (Map String AnyComorphism -> [AnyComorphism])
-> Map String AnyComorphism -> [AnyComorphism]
forall a b. (a -> b) -> a -> b
$ LogicGraph -> Map String AnyComorphism
comorphisms LogicGraph
lg
      groupC :: [(G_sublogics, [a])] -> [(G_sublogics, [a])]
groupC = Map G_sublogics [a] -> [(G_sublogics, [a])]
forall k a. Map k a -> [(k, a)]
Map.toList (Map G_sublogics [a] -> [(G_sublogics, [a])])
-> ([(G_sublogics, [a])] -> Map G_sublogics [a])
-> [(G_sublogics, [a])]
-> [(G_sublogics, [a])]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([a] -> [a] -> [a]) -> [(G_sublogics, [a])] -> Map G_sublogics [a]
forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
Map.fromListWith [a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
(++)
      ssubs :: [(G_sublogics, [String])]
ssubs = [(G_sublogics, [String])] -> [(G_sublogics, [String])]
forall a. [(G_sublogics, [a])] -> [(G_sublogics, [a])]
groupC
        ([(G_sublogics, [String])] -> [(G_sublogics, [String])])
-> [(G_sublogics, [String])] -> [(G_sublogics, [String])]
forall a b. (a -> b) -> a -> b
$ (AnyComorphism -> (G_sublogics, [String]))
-> [AnyComorphism] -> [(G_sublogics, [String])]
forall a b. (a -> b) -> [a] -> [b]
map (\ (Comorphism cid :: cid
cid) -> (lid1 -> sublogics1 -> G_sublogics
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> sublogics -> G_sublogics
G_sublogics (cid -> lid1
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 -> lid1
sourceLogic cid
cid)
           (sublogics1 -> G_sublogics) -> sublogics1 -> G_sublogics
forall a b. (a -> b) -> a -> b
$ cid -> sublogics1
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 -> sublogics1
sourceSublogic cid
cid, [cid -> String
forall lid. Language lid => lid -> String
language_name cid
cid])) [AnyComorphism]
cs
      tsubs :: [(G_sublogics, [String])]
tsubs = [(G_sublogics, [String])] -> [(G_sublogics, [String])]
forall a. [(G_sublogics, [a])] -> [(G_sublogics, [a])]
groupC
        ([(G_sublogics, [String])] -> [(G_sublogics, [String])])
-> [(G_sublogics, [String])] -> [(G_sublogics, [String])]
forall a b. (a -> b) -> a -> b
$ (AnyComorphism -> (G_sublogics, [String]))
-> [AnyComorphism] -> [(G_sublogics, [String])]
forall a b. (a -> b) -> [a] -> [b]
map (\ (Comorphism cid :: cid
cid) -> (lid2 -> sublogics2 -> G_sublogics
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> sublogics -> G_sublogics
G_sublogics (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)
           (sublogics2 -> G_sublogics) -> sublogics2 -> G_sublogics
forall a b. (a -> b) -> a -> b
$ cid -> sublogics2
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 -> sublogics2
targetSublogic cid
cid, [cid -> String
forall lid. Language lid => lid -> String
language_name cid
cid])) [AnyComorphism]
cs
  [Json]
ls <- (AnyLogic -> IO Json) -> [AnyLogic] -> IO [Json]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM AnyLogic -> IO Json
logicToJson ([AnyLogic] -> IO [Json])
-> (Map String AnyLogic -> [AnyLogic])
-> Map String AnyLogic
-> IO [Json]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map String AnyLogic -> [AnyLogic]
forall k a. Map k a -> [a]
Map.elems (Map String AnyLogic -> IO [Json])
-> Map String AnyLogic -> IO [Json]
forall a b. (a -> b) -> a -> b
$ LogicGraph -> Map String AnyLogic
logics LogicGraph
lg
  Json -> IO Json
forall (m :: * -> *) a. Monad m => a -> m a
return (Json -> IO Json) -> Json -> IO Json
forall a b. (a -> b) -> a -> b
$ [JPair] -> Json
mkJObj [("logic_graph", [JPair] -> Json
mkJObj
    [ ("logics", [Json] -> Json
mkJArr [Json]
ls)
    , ("source_sublogics", [Json] -> Json
mkJArr ([Json] -> Json) -> [Json] -> Json
forall a b. (a -> b) -> a -> b
$ ((G_sublogics, [String]) -> Json)
-> [(G_sublogics, [String])] -> [Json]
forall a b. (a -> b) -> [a] -> [b]
map (\ (a :: G_sublogics
a, ns :: [String]
ns) -> [JPair] -> Json
mkJObj
             [ String -> JPair
mkNameJPair (String -> JPair) -> String -> JPair
forall a b. (a -> b) -> a -> b
$ G_sublogics -> String
forall a. Show a => a -> String
show G_sublogics
a
             , ("comorphisms", [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]
ns)]) [(G_sublogics, [String])]
ssubs)
    , ("target_sublogics", [Json] -> Json
mkJArr ([Json] -> Json) -> [Json] -> Json
forall a b. (a -> b) -> a -> b
$ ((G_sublogics, [String]) -> Json)
-> [(G_sublogics, [String])] -> [Json]
forall a b. (a -> b) -> [a] -> [b]
map (\ (a :: G_sublogics
a, ns :: [String]
ns) -> [JPair] -> Json
mkJObj
             [ String -> JPair
mkNameJPair (String -> JPair) -> String -> JPair
forall a b. (a -> b) -> a -> b
$ G_sublogics -> String
forall a. Show a => a -> String
show G_sublogics
a
             , ("comorphisms", [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]
ns)]) [(G_sublogics, [String])]
tsubs)
    , ("comorphisms", [Json] -> Json
mkJArr ([Json] -> Json) -> [Json] -> Json
forall a b. (a -> b) -> a -> b
$ (AnyComorphism -> Json) -> [AnyComorphism] -> [Json]
forall a b. (a -> b) -> [a] -> [b]
map AnyComorphism -> Json
comorphismToJson [AnyComorphism]
cs)] )]

logicToJson :: AnyLogic -> IO Json
logicToJson :: AnyLogic -> IO Json
logicToJson (Logic lid :: lid
lid) = do
 let ps :: [Prover sign sentence morphism sublogics proof_tree]
ps = lid -> [Prover sign sentence morphism sublogics proof_tree]
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> [Prover sign sentence morphism sublogics proof_tree]
provers lid
lid
     cs1 :: [ConsChecker sign sentence sublogics morphism proof_tree]
cs1 = lid -> [ConsChecker sign sentence sublogics morphism proof_tree]
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> [ConsChecker sign sentence sublogics morphism proof_tree]
cons_checkers lid
lid
     cs2 :: [ConservativityChecker sign sentence morphism]
cs2 = lid -> [ConservativityChecker sign sentence morphism]
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> [ConservativityChecker sign sentence morphism]
conservativityCheck lid
lid
     ua :: Maybe a -> JPair
ua b :: Maybe a
b = ("usable", Bool -> Json
mkJBool (Bool -> Json) -> Bool -> Json
forall a b. (a -> b) -> a -> b
$ Maybe a -> Bool
forall a. Maybe a -> Bool
isNothing Maybe a
b)
 [Maybe String]
bps <- (Prover sign sentence morphism sublogics proof_tree
 -> IO (Maybe String))
-> [Prover sign sentence morphism sublogics proof_tree]
-> IO [Maybe String]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Prover sign sentence morphism sublogics proof_tree
-> IO (Maybe String)
forall theory sentence morphism sublogics proof_tree.
ProverTemplate theory sentence morphism sublogics proof_tree
-> IO (Maybe String)
proverUsable [Prover sign sentence morphism sublogics proof_tree]
ps
 [Maybe String]
bcs1 <- (ConsChecker sign sentence sublogics morphism proof_tree
 -> IO (Maybe String))
-> [ConsChecker sign sentence sublogics morphism proof_tree]
-> IO [Maybe String]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ConsChecker sign sentence sublogics morphism proof_tree
-> IO (Maybe String)
forall sign sentence sublogics morphism proof_tree.
ConsChecker sign sentence sublogics morphism proof_tree
-> IO (Maybe String)
ccUsable [ConsChecker sign sentence sublogics morphism proof_tree]
cs1
 [Maybe String]
bcs2 <- (ConservativityChecker sign sentence morphism -> IO (Maybe String))
-> [ConservativityChecker sign sentence morphism]
-> IO [Maybe String]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ConservativityChecker sign sentence morphism -> IO (Maybe String)
forall sign sentence morphism.
ConservativityChecker sign sentence morphism -> IO (Maybe String)
checkerUsable [ConservativityChecker sign sentence morphism]
cs2
 Json -> IO Json
forall (m :: * -> *) a. Monad m => a -> m a
return (Json -> IO Json) -> Json -> IO Json
forall a b. (a -> b) -> a -> b
$ [JPair] -> Json
mkJObj
  [ String -> JPair
mkNameJPair (String -> JPair) -> String -> JPair
forall a b. (a -> b) -> a -> b
$ lid -> String
forall lid. Language lid => lid -> String
language_name lid
lid
  , String -> String -> JPair
mkJPair "Stability" (String -> JPair) -> (Stability -> String) -> Stability -> JPair
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Stability -> String
forall a. Show a => a -> String
show (Stability -> JPair) -> Stability -> JPair
forall a b. (a -> b) -> a -> b
$ lid -> Stability
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> Stability
stability lid
lid
  , ("has_basic_parser", Bool -> Json
mkJBool (Bool -> Json)
-> (Map
      String (PrefixMap -> AParser Any basic_spec, basic_spec -> Doc)
    -> Bool)
-> Map
     String (PrefixMap -> AParser Any basic_spec, basic_spec -> Doc)
-> Json
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> Bool
not (Bool -> Bool)
-> (Map
      String (PrefixMap -> AParser Any basic_spec, basic_spec -> Doc)
    -> Bool)
-> Map
     String (PrefixMap -> AParser Any basic_spec, basic_spec -> Doc)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map String (PrefixMap -> AParser Any basic_spec, basic_spec -> Doc)
-> Bool
forall k a. Map k a -> Bool
Map.null (Map
   String (PrefixMap -> AParser Any basic_spec, basic_spec -> Doc)
 -> Json)
-> Map
     String (PrefixMap -> AParser Any basic_spec, basic_spec -> Doc)
-> Json
forall a b. (a -> b) -> a -> b
$ lid
-> Map
     String (PrefixMap -> AParser Any basic_spec, basic_spec -> Doc)
forall lid basic_spec symbol symb_items symb_map_items st.
Syntax lid basic_spec symbol symb_items symb_map_items =>
lid
-> Map
     String (PrefixMap -> AParser st basic_spec, basic_spec -> Doc)
parsersAndPrinters lid
lid)
  , ("has_basic_analysis", Bool -> Json
mkJBool (Bool -> Json)
-> (Maybe
      ((basic_spec, sign, GlobalAnnos)
       -> Result (basic_spec, ExtSign sign symbol, [Named sentence]))
    -> Bool)
-> Maybe
     ((basic_spec, sign, GlobalAnnos)
      -> Result (basic_spec, ExtSign sign symbol, [Named sentence]))
-> Json
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe
  ((basic_spec, sign, GlobalAnnos)
   -> Result (basic_spec, ExtSign sign symbol, [Named sentence]))
-> Bool
forall a. Maybe a -> Bool
isJust (Maybe
   ((basic_spec, sign, GlobalAnnos)
    -> Result (basic_spec, ExtSign sign symbol, [Named sentence]))
 -> Json)
-> Maybe
     ((basic_spec, sign, GlobalAnnos)
      -> Result (basic_spec, ExtSign sign symbol, [Named sentence]))
-> Json
forall a b. (a -> b) -> a -> b
$ lid
-> Maybe
     ((basic_spec, sign, GlobalAnnos)
      -> Result (basic_spec, ExtSign sign symbol, [Named sentence]))
forall lid basic_spec sentence symb_items symb_map_items sign
       morphism symbol raw_symbol.
StaticAnalysis
  lid
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol =>
lid
-> Maybe
     ((basic_spec, sign, GlobalAnnos)
      -> Result (basic_spec, ExtSign sign symbol, [Named sentence]))
basic_analysis lid
lid)
  , ("has_symbol_list_parser", Bool -> Json
mkJBool (Bool -> Json)
-> (Maybe (PrefixMap -> AParser Any symb_items) -> Bool)
-> Maybe (PrefixMap -> AParser Any symb_items)
-> Json
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe (PrefixMap -> AParser Any symb_items) -> Bool
forall a. Maybe a -> Bool
isJust (Maybe (PrefixMap -> AParser Any symb_items) -> Json)
-> Maybe (PrefixMap -> AParser Any symb_items) -> Json
forall a b. (a -> b) -> a -> b
$ lid -> Maybe (PrefixMap -> AParser Any symb_items)
forall lid basic_spec symbol symb_items symb_map_items st.
Syntax lid basic_spec symbol symb_items symb_map_items =>
lid -> Maybe (PrefixMap -> AParser st symb_items)
parse_symb_items lid
lid)
  , ("has_symbol_map_parser", Bool -> Json
mkJBool (Bool -> Json)
-> (Maybe (PrefixMap -> AParser Any symb_map_items) -> Bool)
-> Maybe (PrefixMap -> AParser Any symb_map_items)
-> Json
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe (PrefixMap -> AParser Any symb_map_items) -> Bool
forall a. Maybe a -> Bool
isJust (Maybe (PrefixMap -> AParser Any symb_map_items) -> Json)
-> Maybe (PrefixMap -> AParser Any symb_map_items) -> Json
forall a b. (a -> b) -> a -> b
$ lid -> Maybe (PrefixMap -> AParser Any symb_map_items)
forall lid basic_spec symbol symb_items symb_map_items st.
Syntax lid basic_spec symbol symb_items symb_map_items =>
lid -> Maybe (PrefixMap -> AParser st symb_map_items)
parse_symb_map_items lid
lid)
  , ("is_a_process_logic", Bool -> Json
mkJBool (Bool -> Json)
-> (Maybe AnyLogic -> Bool) -> Maybe AnyLogic -> Json
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe AnyLogic -> Bool
forall a. Maybe a -> Bool
isJust (Maybe AnyLogic -> Json) -> Maybe AnyLogic -> Json
forall a b. (a -> b) -> a -> b
$ lid -> Maybe AnyLogic
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> Maybe AnyLogic
data_logic lid
lid)
  , ("description_lines", [Json] -> Json
mkJArr ([Json] -> Json) -> (String -> [Json]) -> String -> Json
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String -> Json) -> [String] -> [Json]
forall a b. (a -> b) -> [a] -> [b]
map String -> Json
mkJStr ([String] -> [Json]) -> (String -> [String]) -> String -> [Json]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> [String]
lines (String -> Json) -> String -> Json
forall a b. (a -> b) -> a -> b
$ lid -> String
forall lid. Language lid => lid -> String
description lid
lid)
  , ("serializations", [Json] -> Json
mkJArr ([Json] -> Json)
-> (Map
      String (PrefixMap -> AParser Any basic_spec, basic_spec -> Doc)
    -> [Json])
-> Map
     String (PrefixMap -> AParser Any basic_spec, basic_spec -> Doc)
-> Json
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String -> Json) -> [String] -> [Json]
forall a b. (a -> b) -> [a] -> [b]
map String -> Json
mkJStr
     ([String] -> [Json])
-> (Map
      String (PrefixMap -> AParser Any basic_spec, basic_spec -> Doc)
    -> [String])
-> Map
     String (PrefixMap -> AParser Any basic_spec, basic_spec -> Doc)
-> [Json]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String -> Bool) -> [String] -> [String]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (String -> Bool) -> String -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null) ([String] -> [String])
-> (Map
      String (PrefixMap -> AParser Any basic_spec, basic_spec -> Doc)
    -> [String])
-> Map
     String (PrefixMap -> AParser Any basic_spec, basic_spec -> Doc)
-> [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map String (PrefixMap -> AParser Any basic_spec, basic_spec -> Doc)
-> [String]
forall k a. Map k a -> [k]
Map.keys (Map
   String (PrefixMap -> AParser Any basic_spec, basic_spec -> Doc)
 -> Json)
-> Map
     String (PrefixMap -> AParser Any basic_spec, basic_spec -> Doc)
-> Json
forall a b. (a -> b) -> a -> b
$ lid
-> Map
     String (PrefixMap -> AParser Any basic_spec, basic_spec -> Doc)
forall lid basic_spec symbol symb_items symb_map_items st.
Syntax lid basic_spec symbol symb_items symb_map_items =>
lid
-> Map
     String (PrefixMap -> AParser st basic_spec, basic_spec -> Doc)
parsersAndPrinters lid
lid)
  , ("provers", [Json] -> Json
mkJArr ([Json] -> Json) -> [Json] -> Json
forall a b. (a -> b) -> a -> b
$ (Prover sign sentence morphism sublogics proof_tree
 -> Maybe String -> Json)
-> [Prover sign sentence morphism sublogics proof_tree]
-> [Maybe String]
-> [Json]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\ a :: Prover sign sentence morphism sublogics proof_tree
a b :: Maybe String
b ->
         [JPair] -> Json
mkJObj [String -> JPair
mkNameJPair (String -> JPair) -> String -> JPair
forall a b. (a -> b) -> a -> b
$ Prover sign sentence morphism sublogics proof_tree -> String
forall theory sentence morphism sublogics proof_tree.
ProverTemplate theory sentence morphism sublogics proof_tree
-> String
proverName Prover sign sentence morphism sublogics proof_tree
a, Maybe String -> JPair
forall a. Maybe a -> JPair
ua Maybe String
b]) [Prover sign sentence morphism sublogics proof_tree]
ps [Maybe String]
bps)
  , ("consistency_checkers", [Json] -> Json
mkJArr ([Json] -> Json) -> [Json] -> Json
forall a b. (a -> b) -> a -> b
$ (ConsChecker sign sentence sublogics morphism proof_tree
 -> Maybe String -> Json)
-> [ConsChecker sign sentence sublogics morphism proof_tree]
-> [Maybe String]
-> [Json]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\ a :: ConsChecker sign sentence sublogics morphism proof_tree
a b :: Maybe String
b ->
         [JPair] -> Json
mkJObj [String -> JPair
mkNameJPair (String -> JPair) -> String -> JPair
forall a b. (a -> b) -> a -> b
$ ConsChecker sign sentence sublogics morphism proof_tree -> String
forall sign sentence sublogics morphism proof_tree.
ConsChecker sign sentence sublogics morphism proof_tree -> String
ccName ConsChecker sign sentence sublogics morphism proof_tree
a, Maybe String -> JPair
forall a. Maybe a -> JPair
ua Maybe String
b]) [ConsChecker sign sentence sublogics morphism proof_tree]
cs1 [Maybe String]
bcs1)
  , ("conservativity_checkers", [Json] -> Json
mkJArr ([Json] -> Json) -> [Json] -> Json
forall a b. (a -> b) -> a -> b
$ (ConservativityChecker sign sentence morphism
 -> Maybe String -> Json)
-> [ConservativityChecker sign sentence morphism]
-> [Maybe String]
-> [Json]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\ a :: ConservativityChecker sign sentence morphism
a b :: Maybe String
b ->
          [JPair] -> Json
mkJObj [String -> JPair
mkNameJPair (String -> JPair) -> String -> JPair
forall a b. (a -> b) -> a -> b
$ ConservativityChecker sign sentence morphism -> String
forall sign sentence morphism.
ConservativityChecker sign sentence morphism -> String
checkerId ConservativityChecker sign sentence morphism
a, Maybe String -> JPair
forall a. Maybe a -> JPair
ua Maybe String
b]) [ConservativityChecker sign sentence morphism]
cs2 [Maybe String]
bcs2)
  , ("sublogics", [Json] -> Json
mkJArr ([Json] -> Json) -> ([sublogics] -> [Json]) -> [sublogics] -> Json
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (sublogics -> Json) -> [sublogics] -> [Json]
forall a b. (a -> b) -> [a] -> [b]
map (String -> Json
mkJStr (String -> Json) -> (sublogics -> String) -> sublogics -> Json
forall b c a. (b -> c) -> (a -> b) -> a -> c
. sublogics -> String
forall l. SublogicName l => l -> String
sublogicName) ([sublogics] -> Json) -> [sublogics] -> Json
forall a b. (a -> b) -> a -> b
$ lid -> [sublogics]
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> [sublogics]
all_sublogics lid
lid)]

comorphismToJson :: AnyComorphism -> Json
comorphismToJson :: AnyComorphism -> Json
comorphismToJson (Comorphism cid :: cid
cid) = [JPair] -> Json
mkJObj
  [ String -> JPair
mkNameJPair (String -> JPair) -> String -> JPair
forall a b. (a -> b) -> a -> b
$ cid -> String
forall lid. Language lid => lid -> String
language_name cid
cid
  , String -> String -> JPair
mkJPair "source" (String -> JPair) -> String -> JPair
forall a b. (a -> b) -> a -> b
$ lid1 -> String
forall lid. Language lid => lid -> String
language_name (cid -> lid1
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 -> lid1
sourceLogic cid
cid)
  , String -> String -> JPair
mkJPair "target" (String -> JPair) -> String -> JPair
forall a b. (a -> b) -> a -> b
$ lid2 -> String
forall lid. Language lid => lid -> String
language_name (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)
  , String -> String -> JPair
mkJPair "sourceSublogic" (String -> JPair) -> (sublogics1 -> String) -> sublogics1 -> JPair
forall b c a. (b -> c) -> (a -> b) -> a -> c
. sublogics1 -> String
forall l. SublogicName l => l -> String
sublogicName (sublogics1 -> JPair) -> sublogics1 -> JPair
forall a b. (a -> b) -> a -> b
$ cid -> sublogics1
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 -> sublogics1
sourceSublogic cid
cid
  , String -> String -> JPair
mkJPair "targetSublogic" (String -> JPair) -> (sublogics2 -> String) -> sublogics2 -> JPair
forall b c a. (b -> c) -> (a -> b) -> a -> c
. sublogics2 -> String
forall l. SublogicName l => l -> String
sublogicName (sublogics2 -> JPair) -> sublogics2 -> JPair
forall a b. (a -> b) -> a -> b
$ cid -> sublogics2
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 -> sublogics2
targetSublogic cid
cid
  , ("is_inclusion", Bool -> Json
mkJBool (Bool -> Json) -> Bool -> Json
forall a b. (a -> b) -> a -> b
$ cid -> Bool
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 -> Bool
isInclusionComorphism cid
cid)
  , ("has_model_expansion", Bool -> Json
mkJBool (Bool -> Json) -> Bool -> Json
forall a b. (a -> b) -> a -> b
$ cid -> Bool
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 -> Bool
has_model_expansion cid
cid)
  , ("is_weakly_amalgamable", Bool -> Json
mkJBool (Bool -> Json) -> Bool -> Json
forall a b. (a -> b) -> a -> b
$ cid -> Bool
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 -> Bool
is_weakly_amalgamable cid
cid)
  ]