{- |
Module      :  ./GUI/ShowLogicGraph.hs
Copyright   :  (c) Heng Jiang and Till Mossakowski, Uni Bremen 2002-2006
License     :  GPLv2 or higher, see LICENSE.txt

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

display the logic graph
-}

module GUI.ShowLogicGraph (showPlainLG, showLG) where

import GUI.UDGUtils as UDG
import GUI.HTkUtils as HTk
import qualified GUI.GraphAbstraction as GA

import HTk.Toolkit.DialogWin (useHTk)

import Comorphisms.LogicGraph
import Comorphisms.LogicList
import Comorphisms.HetLogicGraph
import Logic.Grothendieck
import Logic.Logic
import Logic.Comorphism
import Logic.Prover

import qualified Data.Map as Map
import Data.List
import qualified Common.Lib.Rel as Rel
import Common.Consistency

import Data.Typeable

graphParms :: GraphAllConfig graph graphParms node nodeType nodeTypeParms
                              arc arcType arcTypeParms
           => Graph graph graphParms node nodeType nodeTypeParms
                        arc arcType arcTypeParms
           -> String -- ^ title of graph
           -> graphParms
graphParms :: Graph
  graph
  graphParms
  node
  nodeType
  nodeTypeParms
  arc
  arcType
  arcTypeParms
-> String -> graphParms
graphParms _ title :: String
title =
             String -> GraphTitle
GraphTitle String
title GraphTitle -> graphParms -> graphParms
forall option configuration.
HasConfig option configuration =>
option -> configuration -> configuration
$$
             Bool -> OptimiseLayout
OptimiseLayout Bool
True OptimiseLayout -> graphParms -> graphParms
forall option configuration.
HasConfig option configuration =>
option -> configuration -> configuration
$$
             IO Bool -> AllowClose
AllowClose (Bool -> IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True) AllowClose -> graphParms -> graphParms
forall option configuration.
HasConfig option configuration =>
option -> configuration -> configuration
$$
             graphParms
forall graphParms. GraphParms graphParms => graphParms
emptyGraphParms

makeNodeMenu :: (GraphAllConfig graph graphParms node
                                    nodeType nodeTypeParms
                                     arc arcType arcTypeParms,
                       Typeable value)
                  => Graph graph graphParms node nodeType nodeTypeParms
                        arc arcType arcTypeParms
                  -> (value -> IO String)
                  -- ^ display the value as a String
                  -> LocalMenu value
                  -> String -- ^ color of node
                  -> nodeTypeParms value
makeNodeMenu :: Graph
  graph
  graphParms
  node
  nodeType
  nodeTypeParms
  arc
  arcType
  arcTypeParms
-> (value -> IO String)
-> LocalMenu value
-> String
-> nodeTypeParms value
makeNodeMenu _ showMyValue :: value -> IO String
showMyValue logicNodeMenu :: LocalMenu value
logicNodeMenu color :: String
color =
               LocalMenu value
logicNodeMenu LocalMenu value -> nodeTypeParms value -> nodeTypeParms value
forall (option :: * -> *) (configuration :: * -> *) value.
(HasConfigValue option configuration, Typeable value) =>
option value -> configuration value -> configuration value
$$$
               Shape value
forall value. Shape value
Ellipse Shape value -> nodeTypeParms value -> nodeTypeParms value
forall (option :: * -> *) (configuration :: * -> *) value.
(HasConfigValue option configuration, Typeable value) =>
option value -> configuration value -> configuration value
$$$
               (value -> IO String) -> ValueTitle value
forall value. (value -> IO String) -> ValueTitle value
ValueTitle value -> IO String
showMyValue ValueTitle value -> nodeTypeParms value -> nodeTypeParms value
forall (option :: * -> *) (configuration :: * -> *) value.
(HasConfigValue option configuration, Typeable value) =>
option value -> configuration value -> configuration value
$$$
               String -> Color value
forall value. String -> Color value
Color String
color Color value -> nodeTypeParms value -> nodeTypeParms value
forall (option :: * -> *) (configuration :: * -> *) value.
(HasConfigValue option configuration, Typeable value) =>
option value -> configuration value -> configuration value
$$$
               nodeTypeParms value
forall (nodeTypeParms :: * -> *) value.
(NodeTypeParms nodeTypeParms, Typeable value) =>
nodeTypeParms value
emptyNodeTypeParms

stableColor, testingColor, unstableColor, experimentalColor,
   proverColor :: String
stableColor :: String
stableColor = "#00FF00"
testingColor :: String
testingColor = "#88FF33"
unstableColor :: String
unstableColor = "#CCFF66"
experimentalColor :: String
experimentalColor = "white"
proverColor :: String
proverColor = "lightsteelblue"

normalArcColor :: String
normalArcColor :: String
normalArcColor = "black"

inclusionArcColor :: String
inclusionArcColor :: String
inclusionArcColor = "blue"

-- | Test whether a comorphism is an ad-hoc inclusion
isInclComorphism :: AnyComorphism -> Bool
isInclComorphism :: AnyComorphism -> Bool
isInclComorphism (Comorphism cid :: cid
cid) =
    lid1 -> 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 -> AnyLogic
Logic (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) AnyLogic -> AnyLogic -> Bool
forall a. Eq a => a -> a -> Bool
== lid2 -> 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 -> AnyLogic
Logic (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) Bool -> Bool -> Bool
&&
    G_sublogics -> G_sublogics -> Bool
isProperSublogic (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) (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))
                      (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) (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))

showLogicGraph :: Bool -> IO GA.OurGraph
showLogicGraph :: Bool -> IO OurGraph
showLogicGraph plain :: Bool
plain = do
           -- disp s tD = debug (s ++ (show tD))
       OurGraph
logicG <- OurGraph -> DaVinciGraphParms -> IO OurGraph
forall graph graphParms (node :: * -> *) (nodeType :: * -> *)
       (nodeTypeParms :: * -> *) (arc :: * -> *) (arcType :: * -> *)
       (arcTypeParms :: * -> *).
GraphAll
  graph
  graphParms
  node
  nodeType
  nodeTypeParms
  arc
  arcType
  arcTypeParms =>
Graph
  graph
  graphParms
  node
  nodeType
  nodeTypeParms
  arc
  arcType
  arcTypeParms
-> graphParms
-> IO
     (Graph
        graph
        graphParms
        node
        nodeType
        nodeTypeParms
        arc
        arcType
        arcTypeParms)
newGraph OurGraph
daVinciSort
                (DaVinciGraphParms -> IO OurGraph)
-> DaVinciGraphParms -> IO OurGraph
forall a b. (a -> b) -> a -> b
$ (if Bool
plain then (MenuPrim (Maybe String) (IO ()) -> GlobalMenu
GlobalMenu (Maybe String
-> [MenuPrim (Maybe String) (IO ())]
-> MenuPrim (Maybe String) (IO ())
forall subMenuValue value.
subMenuValue
-> [MenuPrim subMenuValue value] -> MenuPrim subMenuValue value
UDG.Menu Maybe String
forall a. Maybe a
Nothing [
                String -> IO () -> MenuPrim (Maybe String) (IO ())
forall subMenuValue value.
String -> value -> MenuPrim subMenuValue value
Button "Show detailed logic graph" IO ()
showHSG ]) GlobalMenu -> DaVinciGraphParms -> DaVinciGraphParms
forall option configuration.
HasConfig option configuration =>
option -> configuration -> configuration
$$)
                else DaVinciGraphParms -> DaVinciGraphParms
forall a. a -> a
id)
                (DaVinciGraphParms -> DaVinciGraphParms)
-> DaVinciGraphParms -> DaVinciGraphParms
forall a b. (a -> b) -> a -> b
$ OurGraph -> String -> DaVinciGraphParms
forall graph graphParms (node :: * -> *) (nodeType :: * -> *)
       (nodeTypeParms :: * -> *) (arc :: * -> *) (arcType :: * -> *)
       (arcTypeParms :: * -> *).
GraphAllConfig
  graph
  graphParms
  node
  nodeType
  nodeTypeParms
  arc
  arcType
  arcTypeParms =>
Graph
  graph
  graphParms
  node
  nodeType
  nodeTypeParms
  arc
  arcType
  arcTypeParms
-> String -> graphParms
graphParms OurGraph
daVinciSort (String -> DaVinciGraphParms) -> String -> DaVinciGraphParms
forall a b. (a -> b) -> a -> b
$ if Bool
plain then "Hets Logic Graph" else
                  "Heterogeneous Sublogic Graph"
       let logicNodeMenu :: LocalMenu G_sublogics
logicNodeMenu = MenuPrim (Maybe String) (G_sublogics -> IO ())
-> LocalMenu G_sublogics
forall value.
MenuPrim (Maybe String) (value -> IO ()) -> LocalMenu value
LocalMenu (MenuPrim (Maybe String) (G_sublogics -> IO ())
 -> LocalMenu G_sublogics)
-> MenuPrim (Maybe String) (G_sublogics -> IO ())
-> LocalMenu G_sublogics
forall a b. (a -> b) -> a -> b
$ Maybe String
-> [MenuPrim (Maybe String) (G_sublogics -> IO ())]
-> MenuPrim (Maybe String) (G_sublogics -> IO ())
forall subMenuValue value.
subMenuValue
-> [MenuPrim subMenuValue value] -> MenuPrim subMenuValue value
UDG.Menu (String -> Maybe String
forall a. a -> Maybe a
Just "Info")
                ([MenuPrim (Maybe String) (G_sublogics -> IO ())]
 -> MenuPrim (Maybe String) (G_sublogics -> IO ()))
-> [MenuPrim (Maybe String) (G_sublogics -> IO ())]
-> MenuPrim (Maybe String) (G_sublogics -> IO ())
forall a b. (a -> b) -> a -> b
$ [String
-> (G_sublogics -> IO ())
-> MenuPrim (Maybe String) (G_sublogics -> IO ())
forall subMenuValue value.
String -> value -> MenuPrim subMenuValue value
Button "Tools" ((G_sublogics -> IO ())
 -> MenuPrim (Maybe String) (G_sublogics -> IO ()))
-> (G_sublogics -> IO ())
-> MenuPrim (Maybe String) (G_sublogics -> IO ())
forall a b. (a -> b) -> a -> b
$ \ slg :: G_sublogics
slg -> let lg :: AnyLogic
lg = G_sublogics -> AnyLogic
toAnyLogic G_sublogics
slg in
                      String -> String -> [Config Editor] -> IO ()
createTextDisplay
                      ("Parsers, Provers and Cons_Checker of "
                       String -> String -> String
forall a. [a] -> [a] -> [a]
++ AnyLogic -> String
forall a. Show a => a -> String
show AnyLogic
lg) (AnyLogic -> String
showTools AnyLogic
lg) [Size -> Config Editor
forall w. HasSize w => Size -> Config w
size (80, 25)]]
                [MenuPrim (Maybe String) (G_sublogics -> IO ())]
-> [MenuPrim (Maybe String) (G_sublogics -> IO ())]
-> [MenuPrim (Maybe String) (G_sublogics -> IO ())]
forall a. [a] -> [a] -> [a]
++ [String
-> (G_sublogics -> IO ())
-> MenuPrim (Maybe String) (G_sublogics -> IO ())
forall subMenuValue value.
String -> value -> MenuPrim subMenuValue value
Button "Sublogic" ((G_sublogics -> IO ())
 -> MenuPrim (Maybe String) (G_sublogics -> IO ()))
-> (G_sublogics -> IO ())
-> MenuPrim (Maybe String) (G_sublogics -> IO ())
forall a b. (a -> b) -> a -> b
$ \ slg :: G_sublogics
slg -> let lg :: AnyLogic
lg = G_sublogics -> AnyLogic
toAnyLogic G_sublogics
slg in
                       String -> String -> [Config Editor] -> IO ()
createTextDisplay ("Sublogics of "
                       String -> String -> String
forall a. [a] -> [a] -> [a]
++ AnyLogic -> String
forall a. Show a => a -> String
show AnyLogic
lg) (AnyLogic -> String
showSublogic AnyLogic
lg) [Size -> Config Editor
forall w. HasSize w => Size -> Config w
size (80, 25)] | Bool
plain]
                [MenuPrim (Maybe String) (G_sublogics -> IO ())]
-> [MenuPrim (Maybe String) (G_sublogics -> IO ())]
-> [MenuPrim (Maybe String) (G_sublogics -> IO ())]
forall a. [a] -> [a] -> [a]
++ [String
-> (G_sublogics -> IO ())
-> MenuPrim (Maybe String) (G_sublogics -> IO ())
forall subMenuValue value.
String -> value -> MenuPrim subMenuValue value
Button "Sublogic Graph" ((G_sublogics -> IO ())
 -> MenuPrim (Maybe String) (G_sublogics -> IO ()))
-> (G_sublogics -> IO ())
-> MenuPrim (Maybe String) (G_sublogics -> IO ())
forall a b. (a -> b) -> a -> b
$ AnyLogic -> IO ()
showSubLogicGraph (AnyLogic -> IO ())
-> (G_sublogics -> AnyLogic) -> G_sublogics -> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. G_sublogics -> AnyLogic
toAnyLogic,
                String
-> (G_sublogics -> IO ())
-> MenuPrim (Maybe String) (G_sublogics -> IO ())
forall subMenuValue value.
String -> value -> MenuPrim subMenuValue value
Button "Description" ((G_sublogics -> IO ())
 -> MenuPrim (Maybe String) (G_sublogics -> IO ()))
-> (G_sublogics -> IO ())
-> MenuPrim (Maybe String) (G_sublogics -> IO ())
forall a b. (a -> b) -> a -> b
$ \ slg :: G_sublogics
slg -> let lg :: AnyLogic
lg = G_sublogics -> AnyLogic
toAnyLogic G_sublogics
slg in
                      String -> String -> [Config Editor] -> IO ()
createTextDisplay
                      ("Description of " String -> String -> String
forall a. [a] -> [a] -> [a]
++ AnyLogic -> String
forall a. Show a => a -> String
show AnyLogic
lg) (AnyLogic -> String
showDescription AnyLogic
lg)
                                      [Size -> Config Editor
forall w. HasSize w => Size -> Config w
size (83, 25)]]
           makeLogicNodeMenu :: String -> DaVinciNodeTypeParms G_sublogics
makeLogicNodeMenu = OurGraph
-> (G_sublogics -> IO String)
-> LocalMenu G_sublogics
-> String
-> DaVinciNodeTypeParms G_sublogics
forall graph graphParms (node :: * -> *) (nodeType :: * -> *)
       (nodeTypeParms :: * -> *) (arc :: * -> *) (arcType :: * -> *)
       (arcTypeParms :: * -> *) value.
(GraphAllConfig
   graph
   graphParms
   node
   nodeType
   nodeTypeParms
   arc
   arcType
   arcTypeParms,
 Typeable value) =>
Graph
  graph
  graphParms
  node
  nodeType
  nodeTypeParms
  arc
  arcType
  arcTypeParms
-> (value -> IO String)
-> LocalMenu value
-> String
-> nodeTypeParms value
makeNodeMenu OurGraph
daVinciSort
             (String -> IO String
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> IO String)
-> (G_sublogics -> String) -> G_sublogics -> IO String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. if Bool
plain then AnyLogic -> String
forall a. Show a => a -> String
show (AnyLogic -> String)
-> (G_sublogics -> AnyLogic) -> G_sublogics -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. G_sublogics -> AnyLogic
toAnyLogic else G_sublogics -> String
forall a. Show a => a -> String
show)
                            LocalMenu G_sublogics
logicNodeMenu
       DaVinciNodeType G_sublogics
stableNodeType <- OurGraph
-> DaVinciNodeTypeParms G_sublogics
-> IO (DaVinciNodeType G_sublogics)
forall graph graphParms (node :: * -> *) (nodeType :: * -> *)
       (nodeTypeParms :: * -> *) (arc :: * -> *) (arcType :: * -> *)
       (arcTypeParms :: * -> *) value.
(GraphAll
   graph
   graphParms
   node
   nodeType
   nodeTypeParms
   arc
   arcType
   arcTypeParms,
 Typeable value) =>
Graph
  graph
  graphParms
  node
  nodeType
  nodeTypeParms
  arc
  arcType
  arcTypeParms
-> nodeTypeParms value -> IO (nodeType value)
newNodeType OurGraph
logicG (DaVinciNodeTypeParms G_sublogics
 -> IO (DaVinciNodeType G_sublogics))
-> DaVinciNodeTypeParms G_sublogics
-> IO (DaVinciNodeType G_sublogics)
forall a b. (a -> b) -> a -> b
$ String -> DaVinciNodeTypeParms G_sublogics
makeLogicNodeMenu String
stableColor
       DaVinciNodeType G_sublogics
testingNodeType <- OurGraph
-> DaVinciNodeTypeParms G_sublogics
-> IO (DaVinciNodeType G_sublogics)
forall graph graphParms (node :: * -> *) (nodeType :: * -> *)
       (nodeTypeParms :: * -> *) (arc :: * -> *) (arcType :: * -> *)
       (arcTypeParms :: * -> *) value.
(GraphAll
   graph
   graphParms
   node
   nodeType
   nodeTypeParms
   arc
   arcType
   arcTypeParms,
 Typeable value) =>
Graph
  graph
  graphParms
  node
  nodeType
  nodeTypeParms
  arc
  arcType
  arcTypeParms
-> nodeTypeParms value -> IO (nodeType value)
newNodeType OurGraph
logicG (DaVinciNodeTypeParms G_sublogics
 -> IO (DaVinciNodeType G_sublogics))
-> DaVinciNodeTypeParms G_sublogics
-> IO (DaVinciNodeType G_sublogics)
forall a b. (a -> b) -> a -> b
$ String -> DaVinciNodeTypeParms G_sublogics
makeLogicNodeMenu String
testingColor
       DaVinciNodeType G_sublogics
unstableNodeType <- OurGraph
-> DaVinciNodeTypeParms G_sublogics
-> IO (DaVinciNodeType G_sublogics)
forall graph graphParms (node :: * -> *) (nodeType :: * -> *)
       (nodeTypeParms :: * -> *) (arc :: * -> *) (arcType :: * -> *)
       (arcTypeParms :: * -> *) value.
(GraphAll
   graph
   graphParms
   node
   nodeType
   nodeTypeParms
   arc
   arcType
   arcTypeParms,
 Typeable value) =>
Graph
  graph
  graphParms
  node
  nodeType
  nodeTypeParms
  arc
  arcType
  arcTypeParms
-> nodeTypeParms value -> IO (nodeType value)
newNodeType OurGraph
logicG (DaVinciNodeTypeParms G_sublogics
 -> IO (DaVinciNodeType G_sublogics))
-> DaVinciNodeTypeParms G_sublogics
-> IO (DaVinciNodeType G_sublogics)
forall a b. (a -> b) -> a -> b
$ String -> DaVinciNodeTypeParms G_sublogics
makeLogicNodeMenu String
unstableColor
       DaVinciNodeType G_sublogics
experimentalNodeType <- OurGraph
-> DaVinciNodeTypeParms G_sublogics
-> IO (DaVinciNodeType G_sublogics)
forall graph graphParms (node :: * -> *) (nodeType :: * -> *)
       (nodeTypeParms :: * -> *) (arc :: * -> *) (arcType :: * -> *)
       (arcTypeParms :: * -> *) value.
(GraphAll
   graph
   graphParms
   node
   nodeType
   nodeTypeParms
   arc
   arcType
   arcTypeParms,
 Typeable value) =>
Graph
  graph
  graphParms
  node
  nodeType
  nodeTypeParms
  arc
  arcType
  arcTypeParms
-> nodeTypeParms value -> IO (nodeType value)
newNodeType OurGraph
logicG (DaVinciNodeTypeParms G_sublogics
 -> IO (DaVinciNodeType G_sublogics))
-> DaVinciNodeTypeParms G_sublogics
-> IO (DaVinciNodeType G_sublogics)
forall a b. (a -> b) -> a -> b
$
                               String -> DaVinciNodeTypeParms G_sublogics
makeLogicNodeMenu String
experimentalColor
       DaVinciNodeType G_sublogics
proverNodeType <-
           OurGraph
-> DaVinciNodeTypeParms G_sublogics
-> IO (DaVinciNodeType G_sublogics)
forall graph graphParms (node :: * -> *) (nodeType :: * -> *)
       (nodeTypeParms :: * -> *) (arc :: * -> *) (arcType :: * -> *)
       (arcTypeParms :: * -> *) value.
(GraphAll
   graph
   graphParms
   node
   nodeType
   nodeTypeParms
   arc
   arcType
   arcTypeParms,
 Typeable value) =>
Graph
  graph
  graphParms
  node
  nodeType
  nodeTypeParms
  arc
  arcType
  arcTypeParms
-> nodeTypeParms value -> IO (nodeType value)
newNodeType OurGraph
logicG (DaVinciNodeTypeParms G_sublogics
 -> IO (DaVinciNodeType G_sublogics))
-> DaVinciNodeTypeParms G_sublogics
-> IO (DaVinciNodeType G_sublogics)
forall a b. (a -> b) -> a -> b
$ String -> DaVinciNodeTypeParms G_sublogics
makeLogicNodeMenu String
proverColor
       HetSublogicGraph
hsGr <- IO HetSublogicGraph
hetSublogicGraph
       let newNode' :: G_sublogics -> IO (DaVinciNode G_sublogics)
newNode' logic :: G_sublogics
logic =
             case G_sublogics -> AnyLogic
toAnyLogic G_sublogics
logic of
               Logic lid :: lid
lid -> if [Prover sign sentence morphism sublogics proof_tree] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([Prover sign sentence morphism sublogics proof_tree] -> Bool)
-> [Prover sign sentence morphism sublogics proof_tree] -> Bool
forall a b. (a -> b) -> a -> b
$ 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 then let
                   nodeType :: DaVinciNodeType G_sublogics
nodeType = case 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 of
                     Stable -> DaVinciNodeType G_sublogics
stableNodeType
                     Testing -> DaVinciNodeType G_sublogics
testingNodeType
                     Unstable -> DaVinciNodeType G_sublogics
unstableNodeType
                     Experimental -> DaVinciNodeType G_sublogics
experimentalNodeType
                   in OurGraph
-> DaVinciNodeType G_sublogics
-> G_sublogics
-> IO (DaVinciNode G_sublogics)
forall graph graphParms (node :: * -> *) (nodeType :: * -> *)
       (nodeTypeParms :: * -> *) (arc :: * -> *) (arcType :: * -> *)
       (arcTypeParms :: * -> *) value.
(GraphAll
   graph
   graphParms
   node
   nodeType
   nodeTypeParms
   arc
   arcType
   arcTypeParms,
 Typeable value) =>
Graph
  graph
  graphParms
  node
  nodeType
  nodeTypeParms
  arc
  arcType
  arcTypeParms
-> nodeType value -> value -> IO (node value)
newNode OurGraph
logicG DaVinciNodeType G_sublogics
nodeType G_sublogics
logic
                 else OurGraph
-> DaVinciNodeType G_sublogics
-> G_sublogics
-> IO (DaVinciNode G_sublogics)
forall graph graphParms (node :: * -> *) (nodeType :: * -> *)
       (nodeTypeParms :: * -> *) (arc :: * -> *) (arcType :: * -> *)
       (arcTypeParms :: * -> *) value.
(GraphAll
   graph
   graphParms
   node
   nodeType
   nodeTypeParms
   arc
   arcType
   arcTypeParms,
 Typeable value) =>
Graph
  graph
  graphParms
  node
  nodeType
  nodeTypeParms
  arc
  arcType
  arcTypeParms
-> nodeType value -> value -> IO (node value)
newNode OurGraph
logicG DaVinciNodeType G_sublogics
proverNodeType G_sublogics
logic
           myMap :: Map String G_sublogics
myMap = if Bool
plain then (AnyLogic -> G_sublogics)
-> Map String AnyLogic -> Map String G_sublogics
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map (\ (Logic l :: lid
l) ->
                                          lid -> sublogics -> 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 lid
l (sublogics -> G_sublogics) -> sublogics -> G_sublogics
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
top_sublogic lid
l)
                     (Map String AnyLogic -> Map String G_sublogics)
-> Map String AnyLogic -> Map String G_sublogics
forall a b. (a -> b) -> a -> b
$ [(String, AnyLogic)] -> Map String AnyLogic
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(String, AnyLogic)] -> Map String AnyLogic)
-> [(String, AnyLogic)] -> Map String AnyLogic
forall a b. (a -> b) -> a -> b
$ (AnyLogic -> (String, AnyLogic))
-> [AnyLogic] -> [(String, AnyLogic)]
forall a b. (a -> b) -> [a] -> [b]
map AnyLogic -> (String, AnyLogic)
addLogicName
                     ([AnyLogic] -> [(String, AnyLogic)])
-> [AnyLogic] -> [(String, AnyLogic)]
forall a b. (a -> b) -> a -> b
$ Map String AnyLogic -> [AnyLogic]
forall k a. Map k a -> [a]
Map.elems (Map String AnyLogic -> [AnyLogic])
-> Map String AnyLogic -> [AnyLogic]
forall a b. (a -> b) -> a -> b
$ LogicGraph -> Map String AnyLogic
logics LogicGraph
logicGraph
                   else HetSublogicGraph -> Map String G_sublogics
sublogicNodes HetSublogicGraph
hsGr

       -- production of the nodes (in a list)
       [DaVinciNode G_sublogics]
nodeList <- (G_sublogics -> IO (DaVinciNode G_sublogics))
-> [G_sublogics] -> IO [DaVinciNode G_sublogics]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM G_sublogics -> IO (DaVinciNode G_sublogics)
newNode' ([G_sublogics] -> IO [DaVinciNode G_sublogics])
-> [G_sublogics] -> IO [DaVinciNode G_sublogics]
forall a b. (a -> b) -> a -> b
$ Map String G_sublogics -> [G_sublogics]
forall k a. Map k a -> [a]
Map.elems Map String G_sublogics
myMap
       -- build the map with the node's name and the node.
       let namesAndNodes :: Map String (DaVinciNode G_sublogics)
namesAndNodes = [(String, DaVinciNode G_sublogics)]
-> Map String (DaVinciNode G_sublogics)
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([String]
-> [DaVinciNode G_sublogics] -> [(String, DaVinciNode G_sublogics)]
forall a b. [a] -> [b] -> [(a, b)]
zip (Map String G_sublogics -> [String]
forall k a. Map k a -> [k]
Map.keys Map String G_sublogics
myMap)
                                             [DaVinciNode G_sublogics]
nodeList)
           lookupLogi :: String -> DaVinciNode G_sublogics
lookupLogi gslStr :: String
gslStr =
               DaVinciNode G_sublogics
-> String
-> Map String (DaVinciNode G_sublogics)
-> DaVinciNode G_sublogics
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault (String -> DaVinciNode G_sublogics
forall a. HasCallStack => String -> a
error "lookupLogi: Logic not found")
                                   String
gslStr
                                   Map String (DaVinciNode G_sublogics)
namesAndNodes
           {- each edge can also show the informations (the
             description of comorphism and names of
             source/target-Logic as well as the sublogics). -}
           logicArcMenu :: LocalMenu AnyComorphism
logicArcMenu =
               MenuPrim (Maybe String) (AnyComorphism -> IO ())
-> LocalMenu AnyComorphism
forall value.
MenuPrim (Maybe String) (value -> IO ()) -> LocalMenu value
LocalMenu (MenuPrim (Maybe String) (AnyComorphism -> IO ())
 -> LocalMenu AnyComorphism)
-> MenuPrim (Maybe String) (AnyComorphism -> IO ())
-> LocalMenu AnyComorphism
forall a b. (a -> b) -> a -> b
$ String
-> (AnyComorphism -> IO ())
-> MenuPrim (Maybe String) (AnyComorphism -> IO ())
forall subMenuValue value.
String -> value -> MenuPrim subMenuValue value
Button "Info"
                 ((AnyComorphism -> IO ())
 -> MenuPrim (Maybe String) (AnyComorphism -> IO ()))
-> (AnyComorphism -> IO ())
-> MenuPrim (Maybe String) (AnyComorphism -> IO ())
forall a b. (a -> b) -> a -> b
$ \ c :: AnyComorphism
c -> String -> String -> [Config Editor] -> IO ()
createTextDisplay (AnyComorphism -> String
forall a. Show a => a -> String
show AnyComorphism
c) (AnyComorphism -> String
showComoDescription AnyComorphism
c)
                              [Size -> Config Editor
forall w. HasSize w => Size -> Config w
size (80, 25)]
           acmName :: AnyComorphism -> m String
acmName (Comorphism cid :: cid
cid) = String -> m String
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> m String) -> String -> m String
forall a b. (a -> b) -> a -> b
$ cid -> String
forall lid. Language lid => lid -> String
language_name cid
cid
           normalArcTypeParms :: DaVinciArcTypeParms AnyComorphism
normalArcTypeParms = LocalMenu AnyComorphism
logicArcMenu LocalMenu AnyComorphism
-> DaVinciArcTypeParms AnyComorphism
-> DaVinciArcTypeParms AnyComorphism
forall (option :: * -> *) (configuration :: * -> *) value.
(HasConfigValue option configuration, Typeable value) =>
option value -> configuration value -> configuration value
$$$         -- normal comorphism
                                String -> Color AnyComorphism
forall value. String -> Color value
Color String
normalArcColor Color AnyComorphism
-> DaVinciArcTypeParms AnyComorphism
-> DaVinciArcTypeParms AnyComorphism
forall (option :: * -> *) (configuration :: * -> *) value.
(HasConfigValue option configuration, Typeable value) =>
option value -> configuration value -> configuration value
$$$
                                (AnyComorphism -> IO String) -> ValueTitle AnyComorphism
forall value. (value -> IO String) -> ValueTitle value
ValueTitle AnyComorphism -> IO String
forall (m :: * -> *). Monad m => AnyComorphism -> m String
acmName ValueTitle AnyComorphism
-> DaVinciArcTypeParms AnyComorphism
-> DaVinciArcTypeParms AnyComorphism
forall (option :: * -> *) (configuration :: * -> *) value.
(HasConfigValue option configuration, Typeable value) =>
option value -> configuration value -> configuration value
$$$
                                DaVinciArcTypeParms AnyComorphism
forall (arcTypeParms :: * -> *) value.
(ArcTypeParms arcTypeParms, Typeable value) =>
arcTypeParms value
emptyArcTypeParms
           insertArcType :: DaVinciArcType value
-> ((String, String), value) -> IO (DaVinciArc value)
insertArcType tp :: DaVinciArcType value
tp ((src :: String
src, trg :: String
trg), acm :: value
acm) =
                  OurGraph
-> DaVinciArcType value
-> value
-> DaVinciNode G_sublogics
-> DaVinciNode G_sublogics
-> IO (DaVinciArc value)
forall graph graphParms (node :: * -> *) (nodeType :: * -> *)
       (nodeTypeParms :: * -> *) (arc :: * -> *) (arcType :: * -> *)
       (arcTypeParms :: * -> *) value nodeFromValue nodeToValue.
(GraphAll
   graph
   graphParms
   node
   nodeType
   nodeTypeParms
   arc
   arcType
   arcTypeParms,
 Typeable value, Typeable nodeFromValue, Typeable nodeToValue) =>
Graph
  graph
  graphParms
  node
  nodeType
  nodeTypeParms
  arc
  arcType
  arcTypeParms
-> arcType value
-> value
-> node nodeFromValue
-> node nodeToValue
-> IO (arc value)
newArc OurGraph
logicG DaVinciArcType value
tp value
acm (String -> DaVinciNode G_sublogics
lookupLogi String
src) (String -> DaVinciNode G_sublogics
lookupLogi String
trg)
           inclArcTypeParms :: DaVinciArcTypeParms AnyComorphism
inclArcTypeParms = LocalMenu AnyComorphism
logicArcMenu LocalMenu AnyComorphism
-> DaVinciArcTypeParms AnyComorphism
-> DaVinciArcTypeParms AnyComorphism
forall (option :: * -> *) (configuration :: * -> *) value.
(HasConfigValue option configuration, Typeable value) =>
option value -> configuration value -> configuration value
$$$           -- inclusion
                               String -> Color AnyComorphism
forall value. String -> Color value
Color String
inclusionArcColor Color AnyComorphism
-> DaVinciArcTypeParms AnyComorphism
-> DaVinciArcTypeParms AnyComorphism
forall (option :: * -> *) (configuration :: * -> *) value.
(HasConfigValue option configuration, Typeable value) =>
option value -> configuration value -> configuration value
$$$
                               (if Bool
plain then DaVinciArcTypeParms AnyComorphism
-> DaVinciArcTypeParms AnyComorphism
forall a. a -> a
id else ((AnyComorphism -> IO String) -> ValueTitle AnyComorphism
forall value. (value -> IO String) -> ValueTitle value
ValueTitle AnyComorphism -> IO String
forall (m :: * -> *). Monad m => AnyComorphism -> m String
acmName ValueTitle AnyComorphism
-> DaVinciArcTypeParms AnyComorphism
-> DaVinciArcTypeParms AnyComorphism
forall (option :: * -> *) (configuration :: * -> *) value.
(HasConfigValue option configuration, Typeable value) =>
option value -> configuration value -> configuration value
$$$))
                               DaVinciArcTypeParms AnyComorphism
forall (arcTypeParms :: * -> *) value.
(ArcTypeParms arcTypeParms, Typeable value) =>
arcTypeParms value
emptyArcTypeParms
       DaVinciArcType AnyComorphism
normalArcType <- OurGraph
-> DaVinciArcTypeParms AnyComorphism
-> IO (DaVinciArcType AnyComorphism)
forall graph graphParms (node :: * -> *) (nodeType :: * -> *)
       (nodeTypeParms :: * -> *) (arc :: * -> *) (arcType :: * -> *)
       (arcTypeParms :: * -> *) value.
(GraphAll
   graph
   graphParms
   node
   nodeType
   nodeTypeParms
   arc
   arcType
   arcTypeParms,
 Typeable value) =>
Graph
  graph
  graphParms
  node
  nodeType
  nodeTypeParms
  arc
  arcType
  arcTypeParms
-> arcTypeParms value -> IO (arcType value)
newArcType OurGraph
logicG DaVinciArcTypeParms AnyComorphism
normalArcTypeParms
       DaVinciArcType AnyComorphism
inclArcType <- OurGraph
-> DaVinciArcTypeParms AnyComorphism
-> IO (DaVinciArcType AnyComorphism)
forall graph graphParms (node :: * -> *) (nodeType :: * -> *)
       (nodeTypeParms :: * -> *) (arc :: * -> *) (arcType :: * -> *)
       (arcTypeParms :: * -> *) value.
(GraphAll
   graph
   graphParms
   node
   nodeType
   nodeTypeParms
   arc
   arcType
   arcTypeParms,
 Typeable value) =>
Graph
  graph
  graphParms
  node
  nodeType
  nodeTypeParms
  arc
  arcType
  arcTypeParms
-> arcTypeParms value -> IO (arcType value)
newArcType OurGraph
logicG DaVinciArcTypeParms AnyComorphism
inclArcTypeParms
       if Bool
plain then do
         let toPair :: AnyComorphism -> ((String, String), AnyComorphism)
toPair co :: AnyComorphism
co@(Comorphism c :: cid
c) = ((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
c)
               , 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
c)), AnyComorphism
co)
             insertComo :: AnyComorphism -> IO (DaVinciArc AnyComorphism)
insertComo = DaVinciArcType AnyComorphism
-> ((String, String), AnyComorphism)
-> IO (DaVinciArc AnyComorphism)
forall value.
Typeable value =>
DaVinciArcType value
-> ((String, String), value) -> IO (DaVinciArc value)
insertArcType DaVinciArcType AnyComorphism
normalArcType (((String, String), AnyComorphism)
 -> IO (DaVinciArc AnyComorphism))
-> (AnyComorphism -> ((String, String), AnyComorphism))
-> AnyComorphism
-> IO (DaVinciArc AnyComorphism)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AnyComorphism -> ((String, String), AnyComorphism)
toPair -- for cormophism
             insertIncl :: AnyComorphism -> IO (DaVinciArc AnyComorphism)
insertIncl = DaVinciArcType AnyComorphism
-> ((String, String), AnyComorphism)
-> IO (DaVinciArc AnyComorphism)
forall value.
Typeable value =>
DaVinciArcType value
-> ((String, String), value) -> IO (DaVinciArc value)
insertArcType DaVinciArcType AnyComorphism
inclArcType (((String, String), AnyComorphism)
 -> IO (DaVinciArc AnyComorphism))
-> (AnyComorphism -> ((String, String), AnyComorphism))
-> AnyComorphism
-> IO (DaVinciArc AnyComorphism)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AnyComorphism -> ((String, String), AnyComorphism)
toPair   -- for inclusion
         (AnyComorphism -> IO (DaVinciArc AnyComorphism))
-> [AnyComorphism] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ AnyComorphism -> IO (DaVinciArc AnyComorphism)
insertIncl [AnyComorphism]
inclusionList
         (AnyComorphism -> IO (DaVinciArc AnyComorphism))
-> [AnyComorphism] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ AnyComorphism -> IO (DaVinciArc AnyComorphism)
insertComo ([AnyComorphism] -> IO ()) -> [AnyComorphism] -> IO ()
forall a b. (a -> b) -> a -> b
$ (AnyComorphism -> Bool) -> [AnyComorphism] -> [AnyComorphism]
forall a. (a -> Bool) -> [a] -> [a]
filter (AnyComorphism -> [AnyComorphism] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [AnyComorphism]
inclusionList) [AnyComorphism]
comorphismList
        else do
         HetSublogicGraph
hsg <- IO HetSublogicGraph
hetSublogicGraph
         let (inclCom :: [((String, String), AnyComorphism)]
inclCom, notInclCom :: [((String, String), AnyComorphism)]
notInclCom) =
               (((String, String), AnyComorphism) -> Bool)
-> [((String, String), AnyComorphism)]
-> ([((String, String), AnyComorphism)],
    [((String, String), AnyComorphism)])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition ((AnyComorphism -> [AnyComorphism] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [AnyComorphism]
inclusionList) (AnyComorphism -> Bool)
-> (((String, String), AnyComorphism) -> AnyComorphism)
-> ((String, String), AnyComorphism)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((String, String), AnyComorphism) -> AnyComorphism
forall a b. (a, b) -> b
snd) ([((String, String), AnyComorphism)]
 -> ([((String, String), AnyComorphism)],
     [((String, String), AnyComorphism)]))
-> [((String, String), AnyComorphism)]
-> ([((String, String), AnyComorphism)],
    [((String, String), AnyComorphism)])
forall a b. (a -> b) -> a -> b
$
               (((String, String), [AnyComorphism])
 -> [((String, String), AnyComorphism)])
-> [((String, String), [AnyComorphism])]
-> [((String, String), AnyComorphism)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\ (x :: (String, String)
x, ys :: [AnyComorphism]
ys) -> [(String, String)]
-> [AnyComorphism] -> [((String, String), AnyComorphism)]
forall a b. [a] -> [b] -> [(a, b)]
zip ((String, String) -> [(String, String)]
forall a. a -> [a]
repeat (String, String)
x) [AnyComorphism]
ys) ([((String, String), [AnyComorphism])]
 -> [((String, String), AnyComorphism)])
-> [((String, String), [AnyComorphism])]
-> [((String, String), AnyComorphism)]
forall a b. (a -> b) -> a -> b
$
                   Map (String, String) [AnyComorphism]
-> [((String, String), [AnyComorphism])]
forall k a. Map k a -> [(k, a)]
Map.toList -- [((String,String),[AnyComorphism])]
                          (HetSublogicGraph -> Map (String, String) [AnyComorphism]
comorphismEdges HetSublogicGraph
hsg)
             (adhocCom :: [((String, String), AnyComorphism)]
adhocCom, normalCom :: [((String, String), AnyComorphism)]
normalCom) =
               (((String, String), AnyComorphism) -> Bool)
-> [((String, String), AnyComorphism)]
-> ([((String, String), AnyComorphism)],
    [((String, String), AnyComorphism)])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition (AnyComorphism -> Bool
isInclComorphism (AnyComorphism -> Bool)
-> (((String, String), AnyComorphism) -> AnyComorphism)
-> ((String, String), AnyComorphism)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((String, String), AnyComorphism) -> AnyComorphism
forall a b. (a, b) -> b
snd) [((String, String), AnyComorphism)]
notInclCom
             adhocInclArcTypeParms :: DaVinciArcTypeParms AnyComorphism
adhocInclArcTypeParms =
                             String -> Color AnyComorphism
forall value. String -> Color value
Color String
inclusionArcColor Color AnyComorphism
-> DaVinciArcTypeParms AnyComorphism
-> DaVinciArcTypeParms AnyComorphism
forall (option :: * -> *) (configuration :: * -> *) value.
(HasConfigValue option configuration, Typeable value) =>
option value -> configuration value -> configuration value
$$$ -- ad-hoc inclusion
                             DaVinciArcTypeParms AnyComorphism
forall (arcTypeParms :: * -> *) value.
(ArcTypeParms arcTypeParms, Typeable value) =>
arcTypeParms value
emptyArcTypeParms
         DaVinciArcType AnyComorphism
adhocInclArcType <- OurGraph
-> DaVinciArcTypeParms AnyComorphism
-> IO (DaVinciArcType AnyComorphism)
forall graph graphParms (node :: * -> *) (nodeType :: * -> *)
       (nodeTypeParms :: * -> *) (arc :: * -> *) (arcType :: * -> *)
       (arcTypeParms :: * -> *) value.
(GraphAll
   graph
   graphParms
   node
   nodeType
   nodeTypeParms
   arc
   arcType
   arcTypeParms,
 Typeable value) =>
Graph
  graph
  graphParms
  node
  nodeType
  nodeTypeParms
  arc
  arcType
  arcTypeParms
-> arcTypeParms value -> IO (arcType value)
newArcType OurGraph
logicG DaVinciArcTypeParms AnyComorphism
adhocInclArcTypeParms
         (((String, String), AnyComorphism)
 -> IO (DaVinciArc AnyComorphism))
-> [((String, String), AnyComorphism)] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (DaVinciArcType AnyComorphism
-> ((String, String), AnyComorphism)
-> IO (DaVinciArc AnyComorphism)
forall value.
Typeable value =>
DaVinciArcType value
-> ((String, String), value) -> IO (DaVinciArc value)
insertArcType DaVinciArcType AnyComorphism
inclArcType) [((String, String), AnyComorphism)]
inclCom
         (((String, String), AnyComorphism)
 -> IO (DaVinciArc AnyComorphism))
-> [((String, String), AnyComorphism)] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (DaVinciArcType AnyComorphism
-> ((String, String), AnyComorphism)
-> IO (DaVinciArc AnyComorphism)
forall value.
Typeable value =>
DaVinciArcType value
-> ((String, String), value) -> IO (DaVinciArc value)
insertArcType DaVinciArcType AnyComorphism
adhocInclArcType) [((String, String), AnyComorphism)]
adhocCom
         (((String, String), AnyComorphism)
 -> IO (DaVinciArc AnyComorphism))
-> [((String, String), AnyComorphism)] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (DaVinciArcType AnyComorphism
-> ((String, String), AnyComorphism)
-> IO (DaVinciArc AnyComorphism)
forall value.
Typeable value =>
DaVinciArcType value
-> ((String, String), value) -> IO (DaVinciArc value)
insertArcType DaVinciArcType AnyComorphism
normalArcType) [((String, String), AnyComorphism)]
normalCom
       OurGraph -> IO ()
forall graph graphParms (node :: * -> *) (nodeType :: * -> *)
       (nodeTypeParms :: * -> *) (arc :: * -> *) (arcType :: * -> *)
       (arcTypeParms :: * -> *).
GraphAll
  graph
  graphParms
  node
  nodeType
  nodeTypeParms
  arc
  arcType
  arcTypeParms =>
Graph
  graph
  graphParms
  node
  nodeType
  nodeTypeParms
  arc
  arcType
  arcTypeParms
-> IO ()
redraw OurGraph
logicG
       OurGraph -> IO OurGraph
forall (m :: * -> *) a. Monad m => a -> m a
return OurGraph
logicG

showSubLogicGraph :: AnyLogic -> IO ()
showSubLogicGraph :: AnyLogic -> IO ()
showSubLogicGraph subl :: AnyLogic
subl =
          case AnyLogic
subl of
            Logic sublid :: lid
sublid ->
              do OurGraph
subLogicG <- OurGraph -> DaVinciGraphParms -> IO OurGraph
forall graph graphParms (node :: * -> *) (nodeType :: * -> *)
       (nodeTypeParms :: * -> *) (arc :: * -> *) (arcType :: * -> *)
       (arcTypeParms :: * -> *).
GraphAll
  graph
  graphParms
  node
  nodeType
  nodeTypeParms
  arc
  arcType
  arcTypeParms =>
Graph
  graph
  graphParms
  node
  nodeType
  nodeTypeParms
  arc
  arcType
  arcTypeParms
-> graphParms
-> IO
     (Graph
        graph
        graphParms
        node
        nodeType
        nodeTypeParms
        arc
        arcType
        arcTypeParms)
newGraph OurGraph
daVinciSort
                   (DaVinciGraphParms -> IO OurGraph)
-> DaVinciGraphParms -> IO OurGraph
forall a b. (a -> b) -> a -> b
$ OurGraph -> String -> DaVinciGraphParms
forall graph graphParms (node :: * -> *) (nodeType :: * -> *)
       (nodeTypeParms :: * -> *) (arc :: * -> *) (arcType :: * -> *)
       (arcTypeParms :: * -> *).
GraphAllConfig
  graph
  graphParms
  node
  nodeType
  nodeTypeParms
  arc
  arcType
  arcTypeParms =>
Graph
  graph
  graphParms
  node
  nodeType
  nodeTypeParms
  arc
  arcType
  arcTypeParms
-> String -> graphParms
graphParms OurGraph
daVinciSort "SubLogic Graph"
                 let listG_Sublogics :: [sublogics]
listG_Sublogics = 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
sublid
                     subNodeMenu :: LocalMenu value
subNodeMenu = MenuPrim (Maybe String) (value -> IO ()) -> LocalMenu value
forall value.
MenuPrim (Maybe String) (value -> IO ()) -> LocalMenu value
LocalMenu (Maybe String
-> [MenuPrim (Maybe String) (value -> IO ())]
-> MenuPrim (Maybe String) (value -> IO ())
forall subMenuValue value.
subMenuValue
-> [MenuPrim subMenuValue value] -> MenuPrim subMenuValue value
UDG.Menu Maybe String
forall a. Maybe a
Nothing [])
                     subNodeTypeParms :: DaVinciNodeTypeParms sublogics
subNodeTypeParms =
                         LocalMenu sublogics
forall value. LocalMenu value
subNodeMenu LocalMenu sublogics
-> DaVinciNodeTypeParms sublogics -> DaVinciNodeTypeParms sublogics
forall (option :: * -> *) (configuration :: * -> *) value.
(HasConfigValue option configuration, Typeable value) =>
option value -> configuration value -> configuration value
$$$
                         Shape sublogics
forall value. Shape value
Ellipse Shape sublogics
-> DaVinciNodeTypeParms sublogics -> DaVinciNodeTypeParms sublogics
forall (option :: * -> *) (configuration :: * -> *) value.
(HasConfigValue option configuration, Typeable value) =>
option value -> configuration value -> configuration value
$$$
                         (sublogics -> IO String) -> ValueTitle sublogics
forall value. (value -> IO String) -> ValueTitle value
ValueTitle (String -> IO String
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> IO String)
-> (sublogics -> String) -> sublogics -> IO String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. sublogics -> String
forall l. SublogicName l => l -> String
sublogicName) ValueTitle sublogics
-> DaVinciNodeTypeParms sublogics -> DaVinciNodeTypeParms sublogics
forall (option :: * -> *) (configuration :: * -> *) value.
(HasConfigValue option configuration, Typeable value) =>
option value -> configuration value -> configuration value
$$$
                         String -> Color sublogics
forall value. String -> Color value
Color "yellow" Color sublogics
-> DaVinciNodeTypeParms sublogics -> DaVinciNodeTypeParms sublogics
forall (option :: * -> *) (configuration :: * -> *) value.
(HasConfigValue option configuration, Typeable value) =>
option value -> configuration value -> configuration value
$$$
                         DaVinciNodeTypeParms sublogics
forall (nodeTypeParms :: * -> *) value.
(NodeTypeParms nodeTypeParms, Typeable value) =>
nodeTypeParms value
emptyNodeTypeParms
                 DaVinciNodeType sublogics
subNodeType <- OurGraph
-> DaVinciNodeTypeParms sublogics -> IO (DaVinciNodeType sublogics)
forall graph graphParms (node :: * -> *) (nodeType :: * -> *)
       (nodeTypeParms :: * -> *) (arc :: * -> *) (arcType :: * -> *)
       (arcTypeParms :: * -> *) value.
(GraphAll
   graph
   graphParms
   node
   nodeType
   nodeTypeParms
   arc
   arcType
   arcTypeParms,
 Typeable value) =>
Graph
  graph
  graphParms
  node
  nodeType
  nodeTypeParms
  arc
  arcType
  arcTypeParms
-> nodeTypeParms value -> IO (nodeType value)
newNodeType OurGraph
subLogicG DaVinciNodeTypeParms sublogics
subNodeTypeParms
                 [DaVinciNode sublogics]
subNodeList <- (sublogics -> IO (DaVinciNode sublogics))
-> [sublogics] -> IO [DaVinciNode sublogics]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (OurGraph
-> DaVinciNodeType sublogics
-> sublogics
-> IO (DaVinciNode sublogics)
forall graph graphParms (node :: * -> *) (nodeType :: * -> *)
       (nodeTypeParms :: * -> *) (arc :: * -> *) (arcType :: * -> *)
       (arcTypeParms :: * -> *) value.
(GraphAll
   graph
   graphParms
   node
   nodeType
   nodeTypeParms
   arc
   arcType
   arcTypeParms,
 Typeable value) =>
Graph
  graph
  graphParms
  node
  nodeType
  nodeTypeParms
  arc
  arcType
  arcTypeParms
-> nodeType value -> value -> IO (node value)
newNode OurGraph
subLogicG DaVinciNodeType sublogics
subNodeType)
                                [sublogics]
listG_Sublogics
                 let slAndNodes :: Map sublogics (DaVinciNode sublogics)
slAndNodes = [(sublogics, DaVinciNode sublogics)]
-> Map sublogics (DaVinciNode sublogics)
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(sublogics, DaVinciNode sublogics)]
 -> Map sublogics (DaVinciNode sublogics))
-> [(sublogics, DaVinciNode sublogics)]
-> Map sublogics (DaVinciNode sublogics)
forall a b. (a -> b) -> a -> b
$
                                  [sublogics]
-> [DaVinciNode sublogics] -> [(sublogics, DaVinciNode sublogics)]
forall a b. [a] -> [b] -> [(a, b)]
zip [sublogics]
listG_Sublogics [DaVinciNode sublogics]
subNodeList
                     lookupSublogic :: sublogics -> DaVinciNode sublogics
lookupSublogic g_sl :: sublogics
g_sl =
                         DaVinciNode sublogics
-> sublogics
-> Map sublogics (DaVinciNode sublogics)
-> DaVinciNode sublogics
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault
                              (String -> DaVinciNode sublogics
forall a. HasCallStack => String -> a
error "lookupSublogic: node not found")
                              sublogics
g_sl Map sublogics (DaVinciNode sublogics)
slAndNodes
                     subArcMenu :: LocalMenu value
subArcMenu = MenuPrim (Maybe String) (value -> IO ()) -> LocalMenu value
forall value.
MenuPrim (Maybe String) (value -> IO ()) -> LocalMenu value
LocalMenu (Maybe String
-> [MenuPrim (Maybe String) (value -> IO ())]
-> MenuPrim (Maybe String) (value -> IO ())
forall subMenuValue value.
subMenuValue
-> [MenuPrim subMenuValue value] -> MenuPrim subMenuValue value
UDG.Menu Maybe String
forall a. Maybe a
Nothing [])
                     subArcTypeParms :: DaVinciArcTypeParms String
subArcTypeParms = LocalMenu String
forall value. LocalMenu value
subArcMenu LocalMenu String
-> DaVinciArcTypeParms String -> DaVinciArcTypeParms String
forall (option :: * -> *) (configuration :: * -> *) value.
(HasConfigValue option configuration, Typeable value) =>
option value -> configuration value -> configuration value
$$$
                                       String -> Color String
forall value. String -> Color value
Color "green" Color String
-> DaVinciArcTypeParms String -> DaVinciArcTypeParms String
forall (option :: * -> *) (configuration :: * -> *) value.
(HasConfigValue option configuration, Typeable value) =>
option value -> configuration value -> configuration value
$$$
                                       DaVinciArcTypeParms String
forall (arcTypeParms :: * -> *) value.
(ArcTypeParms arcTypeParms, Typeable value) =>
arcTypeParms value
emptyArcTypeParms
                 DaVinciArcType String
subArcType <- OurGraph
-> DaVinciArcTypeParms String -> IO (DaVinciArcType String)
forall graph graphParms (node :: * -> *) (nodeType :: * -> *)
       (nodeTypeParms :: * -> *) (arc :: * -> *) (arcType :: * -> *)
       (arcTypeParms :: * -> *) value.
(GraphAll
   graph
   graphParms
   node
   nodeType
   nodeTypeParms
   arc
   arcType
   arcTypeParms,
 Typeable value) =>
Graph
  graph
  graphParms
  node
  nodeType
  nodeTypeParms
  arc
  arcType
  arcTypeParms
-> arcTypeParms value -> IO (arcType value)
newArcType OurGraph
subLogicG DaVinciArcTypeParms String
subArcTypeParms
                 let insertSubArc :: (sublogics, sublogics) -> IO (DaVinciArc String)
insertSubArc (node1 :: sublogics
node1, node2 :: sublogics
node2) =
                           OurGraph
-> DaVinciArcType String
-> String
-> DaVinciNode sublogics
-> DaVinciNode sublogics
-> IO (DaVinciArc String)
forall graph graphParms (node :: * -> *) (nodeType :: * -> *)
       (nodeTypeParms :: * -> *) (arc :: * -> *) (arcType :: * -> *)
       (arcTypeParms :: * -> *) value nodeFromValue nodeToValue.
(GraphAll
   graph
   graphParms
   node
   nodeType
   nodeTypeParms
   arc
   arcType
   arcTypeParms,
 Typeable value, Typeable nodeFromValue, Typeable nodeToValue) =>
Graph
  graph
  graphParms
  node
  nodeType
  nodeTypeParms
  arc
  arcType
  arcTypeParms
-> arcType value
-> value
-> node nodeFromValue
-> node nodeToValue
-> IO (arc value)
newArc OurGraph
subLogicG DaVinciArcType String
subArcType String
""
                                  (sublogics -> DaVinciNode sublogics
lookupSublogic sublogics
node1)
                                  (sublogics -> DaVinciNode sublogics
lookupSublogic sublogics
node2)
                     subl_nodes :: [(sublogics, sublogics)]
subl_nodes =
                         Rel sublogics -> [(sublogics, sublogics)]
forall a. Rel a -> [(a, a)]
Rel.toList (Rel sublogics -> [(sublogics, sublogics)])
-> Rel sublogics -> [(sublogics, sublogics)]
forall a b. (a -> b) -> a -> b
$ Rel sublogics -> Rel sublogics
forall a. Ord a => Rel a -> Rel a
Rel.intransKernel (Rel sublogics -> Rel sublogics) -> Rel sublogics -> Rel sublogics
forall a b. (a -> b) -> a -> b
$ [(sublogics, sublogics)] -> Rel sublogics
forall a. Ord a => [(a, a)] -> Rel a
Rel.fromList
                          [ (sublogics
g1, sublogics
g2)
                            | sublogics
g1 <- [sublogics]
listG_Sublogics
                            , sublogics
g2 <- [sublogics]
listG_Sublogics
                            , sublogics
g1 sublogics -> sublogics -> Bool
forall a. Eq a => a -> a -> Bool
/= sublogics
g2
                            , sublogics -> sublogics -> Bool
forall l. SemiLatticeWithTop l => l -> l -> Bool
isSubElem sublogics
g1 sublogics
g2
                          ]
                 ((sublogics, sublogics) -> IO (DaVinciArc String))
-> [(sublogics, sublogics)] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (sublogics, sublogics) -> IO (DaVinciArc String)
insertSubArc [(sublogics, sublogics)]
subl_nodes
                 OurGraph -> IO ()
forall graph graphParms (node :: * -> *) (nodeType :: * -> *)
       (nodeTypeParms :: * -> *) (arc :: * -> *) (arcType :: * -> *)
       (arcTypeParms :: * -> *).
GraphAll
  graph
  graphParms
  node
  nodeType
  nodeTypeParms
  arc
  arcType
  arcTypeParms =>
Graph
  graph
  graphParms
  node
  nodeType
  nodeTypeParms
  arc
  arcType
  arcTypeParms
-> IO ()
redraw OurGraph
subLogicG

toAnyLogic :: G_sublogics -> AnyLogic
toAnyLogic :: G_sublogics -> AnyLogic
toAnyLogic (G_sublogics lid :: lid
lid _) = lid -> 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 -> AnyLogic
Logic lid
lid

showSublogic :: AnyLogic -> String
showSublogic :: AnyLogic -> String
showSublogic (Logic lid :: lid
lid) = [String] -> String
unlines ((sublogics -> String) -> [sublogics] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map sublogics -> String
forall l. SublogicName l => l -> String
sublogicName (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))

showSubTitle :: G_sublogics -> String
showSubTitle :: G_sublogics -> String
showSubTitle (G_sublogics _ lid :: sublogics
lid) = sublogics -> String
forall l. SublogicName l => l -> String
sublogicName sublogics
lid

showDescription :: AnyLogic -> String
showDescription :: AnyLogic -> String
showDescription (Logic lid :: lid
lid) = let s :: String
s = lid -> String
forall lid. Language lid => lid -> String
description lid
lid in
    (if String -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
s then "No description available" else String
s) String -> String -> String
forall a. [a] -> [a] -> [a]
++ "\n\nStability: "
    String -> String -> String
forall a. [a] -> [a] -> [a]
++ Stability -> String
forall a. Show a => a -> String
show (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)

showComoDescription :: AnyComorphism -> String
showComoDescription :: AnyComorphism -> String
showComoDescription (Comorphism cid :: cid
cid) =
  let ssid :: G_sublogics
ssid = 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) (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)
      tsid :: G_sublogics
tsid = 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) (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)
      s :: String
s = cid -> String
forall lid. Language lid => lid -> String
description cid
cid
  in (if String -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
s then "" else String
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ "\n\n")
  String -> String -> String
forall a. [a] -> [a] -> [a]
++ "source logic:     " String -> String -> String
forall a. [a] -> [a] -> [a]
++ 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 -> String
forall a. [a] -> [a] -> [a]
++ "\n\n"
  String -> String -> String
forall a. [a] -> [a] -> [a]
++ "target logic:     " String -> String -> String
forall a. [a] -> [a] -> [a]
++ 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 -> String
forall a. [a] -> [a] -> [a]
++ "\n"
  String -> String -> String
forall a. [a] -> [a] -> [a]
++ "source sublogic:  " String -> String -> String
forall a. [a] -> [a] -> [a]
++ G_sublogics -> String
showSubTitle G_sublogics
ssid String -> String -> String
forall a. [a] -> [a] -> [a]
++ "\n"
  String -> String -> String
forall a. [a] -> [a] -> [a]
++ "target sublogic:  " String -> String -> String
forall a. [a] -> [a] -> [a]
++ G_sublogics -> String
showSubTitle G_sublogics
tsid

showTools :: AnyLogic -> String
showTools :: AnyLogic -> String
showTools (Logic li :: lid
li) =
    case 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
li of
      s :: [String]
s@(_ : r :: [String]
r) -> "Parser for basic specifications.\n"
        String -> String -> String
forall a. [a] -> [a] -> [a]
++ if [String] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [String]
r then "" else
           [String] -> String
unlines ([String] -> String)
-> ([String] -> [String]) -> [String] -> String
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) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ "Additional serializations:"
             String -> [String] -> [String]
forall a. a -> [a] -> [a]
: (String -> String) -> [String] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map String -> String
forall a. Show a => a -> String
show [String]
s
      [] -> ""
  String -> String -> String
forall a. [a] -> [a] -> [a]
++ case 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
li of
       Just _ -> "Parser for symbol lists.\n"
       Nothing -> ""
  String -> String -> String
forall a. [a] -> [a] -> [a]
++ case 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
li of
       Just _ -> "Parser for symbol maps.\n"
       Nothing -> ""
  String -> String -> String
forall a. [a] -> [a] -> [a]
++ case 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
li of
       Just _ -> "Analysis of basic specifications.\n"
       Nothing -> ""
  String -> String -> String
forall a. [a] -> [a] -> [a]
++ case 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
li of
       Just _ -> "is a process logic.\n"
       Nothing -> ""
  String -> String -> String
forall a. [a] -> [a] -> [a]
++ case 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
li of
       [] -> ""
       ls :: [Prover sign sentence morphism sublogics proof_tree]
ls -> [String] -> String
unlines ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ "\nProvers:" String -> [String] -> [String]
forall a. a -> [a] -> [a]
: (Prover sign sentence morphism sublogics proof_tree -> String)
-> [Prover sign sentence morphism sublogics proof_tree] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map 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]
ls
  String -> String -> String
forall a. [a] -> [a] -> [a]
++ case 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
li of
       [] -> ""
       ls :: [ConsChecker sign sentence sublogics morphism proof_tree]
ls -> [String] -> String
unlines ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ "\nConsistency checkers:" String -> [String] -> [String]
forall a. a -> [a] -> [a]
: (ConsChecker sign sentence sublogics morphism proof_tree -> String)
-> [ConsChecker sign sentence sublogics morphism proof_tree]
-> [String]
forall a b. (a -> b) -> [a] -> [b]
map 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]
ls
  String -> String -> String
forall a. [a] -> [a] -> [a]
++ case 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
li of
       [] -> ""
       ls :: [ConservativityChecker sign sentence morphism]
ls -> [String] -> String
unlines ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ "\nConservatity checkers:" String -> [String] -> [String]
forall a. a -> [a] -> [a]
: (ConservativityChecker sign sentence morphism -> String)
-> [ConservativityChecker sign sentence morphism] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map ConservativityChecker sign sentence morphism -> String
forall sign sentence morphism.
ConservativityChecker sign sentence morphism -> String
checkerId [ConservativityChecker sign sentence morphism]
ls


showHSG :: IO ()
showHSG :: IO ()
showHSG = Bool -> IO OurGraph
showLogicGraph Bool
False IO OurGraph -> IO () -> IO ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()

showLG :: IO ()
showLG :: IO ()
showLG = Bool -> IO OurGraph
showLogicGraph Bool
True IO OurGraph -> IO () -> IO ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()

showPlainLG :: IO ()
showPlainLG :: IO ()
showPlainLG = do
  HTk
wishInst <- [Config HTk] -> IO HTk
HTk.initHTk [Config HTk
HTk.withdrawMainWin]
  IO ()
useHTk
  OurGraph
lg <- Bool -> IO OurGraph
showLogicGraph Bool
True
  Event () -> IO ()
forall a. Event a -> IO a
sync (OurGraph -> Event ()
forall o. Destructible o => o -> Event ()
destroyed OurGraph
lg)
  HTk -> IO ()
forall o. Destroyable o => o -> IO ()
destroy HTk
wishInst