{- |
Module      :  ./GUI/Taxonomy.hs
Copyright   :  (c) Klaus Luettich, Uni Bremen 2002-2004
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  luecke@informatik.uni-bremen.de
Stability   :  provisional
Portability :  non-portable (imports Logic)

This module provides the access to Achim Mahnke's taxonomy
visualisation for subsort hierarchies.

-}

module GUI.Taxonomy where


import Logic.Logic
import Logic.Prover
import Static.GTheory

import Taxonomy.MMiSSOntology
import Taxonomy.MMiSSOntologyGraph
import GUI.Utils

import Common.Taxonomy
import Common.Result as Res
import Common.ExtSign

displayConceptGraph :: String -> G_theory -> IO ()
displayConceptGraph :: String -> G_theory -> IO ()
displayConceptGraph = TaxoGraphKind -> String -> G_theory -> IO ()
displayGraph TaxoGraphKind
KConcept

displaySubsortGraph :: String -> G_theory -> IO ()
displaySubsortGraph :: String -> G_theory -> IO ()
displaySubsortGraph = TaxoGraphKind -> String -> G_theory -> IO ()
displayGraph TaxoGraphKind
KSubsort

displayGraph :: TaxoGraphKind -> String -> G_theory -> IO ()
displayGraph :: TaxoGraphKind -> String -> G_theory -> IO ()
displayGraph kind :: TaxoGraphKind
kind thyName :: String
thyName (G_theory lid :: lid
lid _ (ExtSign sign :: sign
sign _) _ sens :: ThSens sentence (AnyComorphism, BasicProof)
sens _) =
    case lid
-> TaxoGraphKind
-> MMiSSOntology
-> sign
-> [Named sentence]
-> Result MMiSSOntology
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
-> TaxoGraphKind
-> MMiSSOntology
-> sign
-> [Named sentence]
-> Result MMiSSOntology
theory_to_taxonomy lid
lid TaxoGraphKind
kind
                       (String -> InsertMode -> MMiSSOntology
emptyMMiSSOntology String
thyName InsertMode
AutoInsert)
                       sign
sign ([Named sentence] -> Result MMiSSOntology)
-> [Named sentence] -> Result MMiSSOntology
forall a b. (a -> b) -> a -> b
$ ThSens sentence (AnyComorphism, BasicProof) -> [Named sentence]
forall a b. ThSens a b -> [Named a]
toNamedList ThSens sentence (AnyComorphism, BasicProof)
sens of
     Res.Result [] (Just taxo :: MMiSSOntology
taxo) -> do
       MMiSSOntology -> Maybe String -> IO OurGraph
displayClassGraph MMiSSOntology
taxo Maybe String
forall a. Maybe a
Nothing
       () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
     Res.Result dias :: [Diagnosis]
dias _ -> String -> String -> IO ()
errorDialog "Error" (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ Int -> [Diagnosis] -> String
showRelDiags 2 [Diagnosis]
dias