{- |
Module      :  ./Logic/LGToXml.hs
Description :  export logic graph information as XML
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 XML
-}

module Logic.LGToXml where

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

import Control.Monad

import qualified Data.Map as Map
import Data.Char
import Data.Maybe

import Common.Consistency
import Common.ToXml

import Text.XML.Light

usableProvers :: LogicGraph -> IO Element
usableProvers :: LogicGraph -> IO Element
usableProvers lg :: LogicGraph
lg = do
  [[Element]]
ps <- (AnyLogic -> IO [Element]) -> [AnyLogic] -> IO [[Element]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM AnyLogic -> IO [Element]
proversOfLogic ([AnyLogic] -> IO [[Element]])
-> (Map String AnyLogic -> [AnyLogic])
-> Map String AnyLogic
-> IO [[Element]]
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 [[Element]])
-> Map String AnyLogic -> IO [[Element]]
forall a b. (a -> b) -> a -> b
$ LogicGraph -> Map String AnyLogic
logics LogicGraph
lg
  Element -> IO Element
forall (m :: * -> *) a. Monad m => a -> m a
return (Element -> IO Element) -> Element -> IO Element
forall a b. (a -> b) -> a -> b
$ String -> [Element] -> Element
forall t. Node t => String -> t -> Element
unode "provers" ([Element] -> Element) -> [Element] -> Element
forall a b. (a -> b) -> a -> b
$ [[Element]] -> [Element]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[Element]]
ps

proversOfLogic :: AnyLogic -> IO [Element]
proversOfLogic :: AnyLogic -> IO [Element]
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
  [Element] -> IO [Element]
forall (m :: * -> *) a. Monad m => a -> m a
return ([Element] -> IO [Element]) -> [Element] -> IO [Element]
forall a b. (a -> b) -> a -> b
$ (ProverTemplate
   (Theory sign sentence proof_tree)
   sentence
   morphism
   sublogics
   proof_tree
 -> Element)
-> [ProverTemplate
      (Theory sign sentence proof_tree)
      sentence
      morphism
      sublogics
      proof_tree]
-> [Element]
forall a b. (a -> b) -> [a] -> [b]
map (\ p :: ProverTemplate
  (Theory sign sentence proof_tree)
  sentence
  morphism
  sublogics
  proof_tree
p ->
      [Attr] -> Element -> Element
add_attrs [ String -> Attr
mkNameAttr (String -> Attr) -> String -> Attr
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 -> Attr
mkAttr "logic" (String -> Attr) -> String -> Attr
forall a b. (a -> b) -> a -> b
$ lid -> String
forall lid. Language lid => lid -> String
language_name lid
lid]
      (Element -> Element) -> Element -> Element
forall a b. (a -> b) -> a -> b
$ String -> () -> Element
forall t. Node t => String -> t -> Element
unode "prover" ()) [ProverTemplate
   (Theory sign sentence proof_tree)
   sentence
   morphism
   sublogics
   proof_tree]
bps

lGToXml :: LogicGraph -> IO Element
lGToXml :: LogicGraph -> IO Element
lGToXml 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
      nameC :: [String] -> [Element]
nameC = (String -> Element) -> [String] -> [Element]
forall a b. (a -> b) -> [a] -> [b]
map (\ n :: String
n -> Attr -> Element -> Element
add_attr (String -> Attr
mkNameAttr String
n) (Element -> Element) -> Element -> Element
forall a b. (a -> b) -> a -> b
$ String -> () -> Element
forall t. Node t => String -> t -> Element
unode "comorphism" ())
  [Element]
ls <- (AnyLogic -> IO Element) -> [AnyLogic] -> IO [Element]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM AnyLogic -> IO Element
logicToXml ([AnyLogic] -> IO [Element])
-> (Map String AnyLogic -> [AnyLogic])
-> Map String AnyLogic
-> IO [Element]
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 [Element])
-> Map String AnyLogic -> IO [Element]
forall a b. (a -> b) -> a -> b
$ LogicGraph -> Map String AnyLogic
logics LogicGraph
lg
  Element -> IO Element
forall (m :: * -> *) a. Monad m => a -> m a
return (Element -> IO Element) -> Element -> IO Element
forall a b. (a -> b) -> a -> b
$ String -> [Element] -> Element
forall t. Node t => String -> t -> Element
unode "LogicGraph"
    ([Element] -> Element) -> [Element] -> Element
forall a b. (a -> b) -> a -> b
$ [Element]
ls
    [Element] -> [Element] -> [Element]
forall a. [a] -> [a] -> [a]
++ ((G_sublogics, [String]) -> Element)
-> [(G_sublogics, [String])] -> [Element]
forall a b. (a -> b) -> [a] -> [b]
map (\ (a :: G_sublogics
a, ns :: [String]
ns) -> Attr -> Element -> Element
add_attr (String -> Attr
mkNameAttr (String -> Attr) -> String -> Attr
forall a b. (a -> b) -> a -> b
$ G_sublogics -> String
forall a. Show a => a -> String
show G_sublogics
a)
          (Element -> Element) -> Element -> Element
forall a b. (a -> b) -> a -> b
$ String -> [Element] -> Element
forall t. Node t => String -> t -> Element
unode "sourceSublogic" ([Element] -> Element) -> [Element] -> Element
forall a b. (a -> b) -> a -> b
$ [String] -> [Element]
nameC [String]
ns) [(G_sublogics, [String])]
ssubs
    [Element] -> [Element] -> [Element]
forall a. [a] -> [a] -> [a]
++ ((G_sublogics, [String]) -> Element)
-> [(G_sublogics, [String])] -> [Element]
forall a b. (a -> b) -> [a] -> [b]
map (\ (a :: G_sublogics
a, ns :: [String]
ns) -> Attr -> Element -> Element
add_attr (String -> Attr
mkNameAttr (String -> Attr) -> String -> Attr
forall a b. (a -> b) -> a -> b
$ G_sublogics -> String
forall a. Show a => a -> String
show G_sublogics
a)
          (Element -> Element) -> Element -> Element
forall a b. (a -> b) -> a -> b
$ String -> [Element] -> Element
forall t. Node t => String -> t -> Element
unode "targetSublogic" ([Element] -> Element) -> [Element] -> Element
forall a b. (a -> b) -> a -> b
$ [String] -> [Element]
nameC [String]
ns) [(G_sublogics, [String])]
tsubs
    [Element] -> [Element] -> [Element]
forall a. [a] -> [a] -> [a]
++ (AnyComorphism -> Element) -> [AnyComorphism] -> [Element]
forall a b. (a -> b) -> [a] -> [b]
map AnyComorphism -> Element
comorphismToXml [AnyComorphism]
cs

logicToXml :: AnyLogic -> IO Element
logicToXml :: AnyLogic -> IO Element
logicToXml (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 -> Attr
ua b :: Maybe a
b = String -> String -> Attr
mkAttr "usable" (String -> Attr) -> (String -> String) -> String -> Attr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Char -> Char) -> String -> String
forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
toLower (String -> Attr) -> String -> Attr
forall a b. (a -> b) -> a -> b
$ Bool -> String
forall a. Show a => a -> String
show (Bool -> String) -> Bool -> String
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
 Element -> IO Element
forall (m :: * -> *) a. Monad m => a -> m a
return (Element -> IO Element) -> Element -> IO Element
forall a b. (a -> b) -> a -> b
$ [Attr] -> Element -> Element
add_attrs
  [ String -> Attr
mkNameAttr (String -> Attr) -> String -> Attr
forall a b. (a -> b) -> a -> b
$ lid -> String
forall lid. Language lid => lid -> String
language_name lid
lid
  , String -> String -> Attr
mkAttr "Stability" (String -> Attr) -> (Stability -> String) -> Stability -> Attr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Stability -> String
forall a. Show a => a -> String
show (Stability -> Attr) -> Stability -> Attr
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
  , String -> String -> Attr
mkAttr "has_basic_parser" (String -> Attr)
-> (Map
      String (PrefixMap -> AParser Any basic_spec, basic_spec -> Doc)
    -> String)
-> Map
     String (PrefixMap -> AParser Any basic_spec, basic_spec -> Doc)
-> Attr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> String
forall a. Show a => a -> String
show (Bool -> String)
-> (Map
      String (PrefixMap -> AParser Any basic_spec, basic_spec -> Doc)
    -> Bool)
-> Map
     String (PrefixMap -> AParser Any basic_spec, basic_spec -> Doc)
-> String
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)
 -> Attr)
-> Map
     String (PrefixMap -> AParser Any basic_spec, basic_spec -> Doc)
-> Attr
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
  , String -> String -> Attr
mkAttr "has_basic_analysis" (String -> Attr)
-> (Maybe
      ((basic_spec, sign, GlobalAnnos)
       -> Result (basic_spec, ExtSign sign symbol, [Named sentence]))
    -> String)
-> Maybe
     ((basic_spec, sign, GlobalAnnos)
      -> Result (basic_spec, ExtSign sign symbol, [Named sentence]))
-> Attr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> String
forall a. Show a => a -> String
show (Bool -> String)
-> (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]))
-> String
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]))
 -> Attr)
-> Maybe
     ((basic_spec, sign, GlobalAnnos)
      -> Result (basic_spec, ExtSign sign symbol, [Named sentence]))
-> Attr
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
  , String -> String -> Attr
mkAttr "has_symbol_list_parser" (String -> Attr)
-> (Maybe (PrefixMap -> AParser Any symb_items) -> String)
-> Maybe (PrefixMap -> AParser Any symb_items)
-> Attr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> String
forall a. Show a => a -> String
show (Bool -> String)
-> (Maybe (PrefixMap -> AParser Any symb_items) -> Bool)
-> Maybe (PrefixMap -> AParser Any symb_items)
-> String
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) -> Attr)
-> Maybe (PrefixMap -> AParser Any symb_items) -> Attr
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
  , String -> String -> Attr
mkAttr "has_symbol_map_parser" (String -> Attr)
-> (Maybe (PrefixMap -> AParser Any symb_map_items) -> String)
-> Maybe (PrefixMap -> AParser Any symb_map_items)
-> Attr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> String
forall a. Show a => a -> String
show (Bool -> String)
-> (Maybe (PrefixMap -> AParser Any symb_map_items) -> Bool)
-> Maybe (PrefixMap -> AParser Any symb_map_items)
-> String
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) -> Attr)
-> Maybe (PrefixMap -> AParser Any symb_map_items) -> Attr
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
  , String -> String -> Attr
mkAttr "is_a_process_logic" (String -> Attr)
-> (Maybe AnyLogic -> String) -> Maybe AnyLogic -> Attr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> String
forall a. Show a => a -> String
show (Bool -> String)
-> (Maybe AnyLogic -> Bool) -> Maybe AnyLogic -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe AnyLogic -> Bool
forall a. Maybe a -> Bool
isJust (Maybe AnyLogic -> Attr) -> Maybe AnyLogic -> Attr
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
  ] (Element -> Element)
-> ([Element] -> Element) -> [Element] -> Element
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> [Element] -> Element
forall t. Node t => String -> t -> Element
unode "logic"
  ([Element] -> Element) -> [Element] -> Element
forall a b. (a -> b) -> a -> b
$ String -> Content -> Element
forall t. Node t => String -> t -> Element
unode "Description" (String -> Content
mkText (String -> Content) -> String -> Content
forall a b. (a -> b) -> a -> b
$ lid -> String
forall lid. Language lid => lid -> String
description lid
lid)
  Element -> [Element] -> [Element]
forall a. a -> [a] -> [a]
: (String -> Element) -> [String] -> [Element]
forall a b. (a -> b) -> [a] -> [b]
map (\ a :: String
a -> Attr -> Element -> Element
add_attr (String -> Attr
mkNameAttr String
a) (Element -> Element) -> Element -> Element
forall a b. (a -> b) -> a -> b
$ String -> () -> Element
forall t. Node t => String -> t -> Element
unode "Serialization" ())
    ((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)
 -> [String])
-> Map
     String (PrefixMap -> AParser Any basic_spec, basic_spec -> Doc)
-> [String]
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)
  [Element] -> [Element] -> [Element]
forall a. [a] -> [a] -> [a]
++ (Prover sign sentence morphism sublogics proof_tree
 -> Maybe String -> Element)
-> [Prover sign sentence morphism sublogics proof_tree]
-> [Maybe String]
-> [Element]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\ a :: Prover sign sentence morphism sublogics proof_tree
a b :: Maybe String
b -> [Attr] -> Element -> Element
add_attrs [String -> Attr
mkNameAttr (String -> Attr) -> String -> Attr
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 -> Attr
forall a. Maybe a -> Attr
ua Maybe String
b]
              (Element -> Element) -> Element -> Element
forall a b. (a -> b) -> a -> b
$ String -> () -> Element
forall t. Node t => String -> t -> Element
unode "Prover" ()) [Prover sign sentence morphism sublogics proof_tree]
ps [Maybe String]
bps
  [Element] -> [Element] -> [Element]
forall a. [a] -> [a] -> [a]
++ (ConsChecker sign sentence sublogics morphism proof_tree
 -> Maybe String -> Element)
-> [ConsChecker sign sentence sublogics morphism proof_tree]
-> [Maybe String]
-> [Element]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\ a :: ConsChecker sign sentence sublogics morphism proof_tree
a b :: Maybe String
b -> [Attr] -> Element -> Element
add_attrs [String -> Attr
mkNameAttr (String -> Attr) -> String -> Attr
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 -> Attr
forall a. Maybe a -> Attr
ua Maybe String
b]
              (Element -> Element) -> Element -> Element
forall a b. (a -> b) -> a -> b
$ String -> () -> Element
forall t. Node t => String -> t -> Element
unode "ConsistencyChecker" ()) [ConsChecker sign sentence sublogics morphism proof_tree]
cs1 [Maybe String]
bcs1
  [Element] -> [Element] -> [Element]
forall a. [a] -> [a] -> [a]
++ (ConservativityChecker sign sentence morphism
 -> Maybe String -> Element)
-> [ConservativityChecker sign sentence morphism]
-> [Maybe String]
-> [Element]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\ a :: ConservativityChecker sign sentence morphism
a b :: Maybe String
b -> [Attr] -> Element -> Element
add_attrs [String -> Attr
mkNameAttr (String -> Attr) -> String -> Attr
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 -> Attr
forall a. Maybe a -> Attr
ua Maybe String
b]
              (Element -> Element) -> Element -> Element
forall a b. (a -> b) -> a -> b
$ String -> () -> Element
forall t. Node t => String -> t -> Element
unode "ConservativityChecker" ()) [ConservativityChecker sign sentence morphism]
cs2 [Maybe String]
bcs2
  [Element] -> [Element] -> [Element]
forall a. [a] -> [a] -> [a]
++ [String -> String -> Element
forall t. Node t => String -> t -> Element
unode "Sublogics" (String -> Element)
-> ([sublogics] -> String) -> [sublogics] -> Element
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [String] -> String
unlines ([String] -> String)
-> ([sublogics] -> [String]) -> [sublogics] -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (sublogics -> String) -> [sublogics] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map sublogics -> String
forall l. SublogicName l => l -> String
sublogicName ([sublogics] -> Element) -> [sublogics] -> Element
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]

comorphismToXml :: AnyComorphism -> Element
comorphismToXml :: AnyComorphism -> Element
comorphismToXml (Comorphism cid :: cid
cid) = [Attr] -> Element -> Element
add_attrs
  [ String -> Attr
mkNameAttr (String -> Attr) -> String -> Attr
forall a b. (a -> b) -> a -> b
$ cid -> String
forall lid. Language lid => lid -> String
language_name cid
cid
  , String -> String -> Attr
mkAttr "source" (String -> Attr) -> String -> Attr
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 -> Attr
mkAttr "target" (String -> Attr) -> String -> Attr
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 -> Attr
mkAttr "sourceSublogic" (String -> Attr) -> (sublogics1 -> String) -> sublogics1 -> Attr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. sublogics1 -> String
forall l. SublogicName l => l -> String
sublogicName (sublogics1 -> Attr) -> sublogics1 -> Attr
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 -> Attr
mkAttr "targetSublogic" (String -> Attr) -> (sublogics2 -> String) -> sublogics2 -> Attr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. sublogics2 -> String
forall l. SublogicName l => l -> String
sublogicName (sublogics2 -> Attr) -> sublogics2 -> Attr
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
  , String -> String -> Attr
mkAttr "is_inclusion" (String -> Attr) -> (Bool -> String) -> Bool -> Attr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> String
forall a. Show a => a -> String
show (Bool -> Attr) -> Bool -> Attr
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
  , String -> String -> Attr
mkAttr "has_model_expansion" (String -> Attr) -> (Bool -> String) -> Bool -> Attr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> String
forall a. Show a => a -> String
show (Bool -> Attr) -> Bool -> Attr
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
  , String -> String -> Attr
mkAttr "is_weakly_amalgamable" (String -> Attr) -> (Bool -> String) -> Bool -> Attr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> String
forall a. Show a => a -> String
show (Bool -> Attr) -> Bool -> Attr
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
  ] (Element -> Element) -> Element -> Element
forall a b. (a -> b) -> a -> b
$ String -> () -> Element
forall t. Node t => String -> t -> Element
unode "comorphism" ()