{- |
Module      :  ./CASL/Taxonomy.hs
Description :  converters for theories to MMiSSOntology
  (subsorting and concept taxonomies)
Copyright   :  (c) Klaus Luettich, Uni Bremen 2002-2004
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  luecke@informatik.uni-bremen.de
Stability   :  provisional
Portability :  portable

Converters for theories to MMiSSOntology (subsorting and concept taxonomies)

the functions showOntClass, showRelationName and showRelation may be used
for printing out MMiSS Ontologies in LaTeX to Stdout
(see commets marked with --printOut).
Please do not remove them without reason!!
-}

module CASL.Taxonomy
  ( -- * Conversion
    convTaxo
    -- * Printing of MMiSS ontologies in LaTeX
  , showOntClass, showRelationName, showRelation) where

import CASL.AS_Basic_CASL
import CASL.Sign

import Taxonomy.MMiSSOntology

import Common.Taxonomy
import Common.Result
import Common.Id ()
import Common.AS_Annotation
import qualified Common.Lib.MapSet as MapSet
import qualified Common.Lib.Rel as Rel

import qualified Data.Map as Map
import qualified Data.Set as Set

{- | convert a generic CASL signature into the MMiSS ontology
datastructure for display as taxonomy graph -}
convTaxo :: TaxoGraphKind -> MMiSSOntology
         -> Sign f e
         -> [Named (FORMULA f)] -> Result MMiSSOntology
convTaxo kind onto sign sens =
   fromWithError $
   case kind of
    KSubsort -> convSign KSubsort onto sign
    KConcept -> foldl convSen (convSign KConcept onto sign) sens

convSign :: TaxoGraphKind
         -> MMiSSOntology -> Sign f e -> WithError MMiSSOntology
convSign KConcept o s =
    case convSign KSubsort o s of
    wOnto -> weither (const wOnto) (convPred s) wOnto
convSign KSubsort onto sign =
    Set.fold addSor (hasValue onto) $ sortSet sign
    -- start with top sorts (maybe use Rel.mostRight?)
    where relMap = Rel.toMap $ Rel.intransKernel $ sortRel sign
          addSor sort weOnto =
             let sortStr = show sort
             in weither (const weOnto)
                        (\ on -> insClass on sortStr
                                          (maybe [] toStrL $
                                                 Map.lookup sort relMap))
                        weOnto
          insClass o nm supL =
              insertClass o nm nm supL (Just SubSort)
          toStrL = map show . Set.toList

convPred :: Sign f e -> MMiSSOntology -> WithError MMiSSOntology
convPred s o =
    -- first only binary preds; later also unary preds
    Map.foldWithKey addPred (hasValue o) $ MapSet.toMap $ predMap s
    where addPred pn tSet wOnto =
           weither (const wOnto) insBinaryPred wOnto
           where insBinaryPred on =
                  let binT = Set.filter isBinPredType tSet
                  in if Set.null binT
                        then hasValue on
                        else Set.fold insType (insName on) binT
                 insName on = insertBaseRelation on (show pn) (show pn)
                                     Nothing Nothing
                 insType t wOn =
                     weither (const wOn)
                             (\ ont ->
                                 let [a1, a2] = predArgs t
                                     src = show a1
                                     tar = show a2
                                 in insertRelationType ont (show pn)
                                       src tar)
                             wOn

convSen :: WithError MMiSSOntology
        -> Named (FORMULA f) -> WithError MMiSSOntology
convSen weOnto _nSen = weither (const weOnto) hasValue weOnto

-- implemented but not used by now
showOntClass :: String -> [String] -> String
showOntClass cln =
    foldl (\ res sup -> res ++ ontClass sup) ""
    where ontClass s = "\\Class{" ++ cln ++ "}{" ++ cln ++ "}{" ++ s ++ "}"

showRelationName :: String -> String
showRelationName rn = "\\RelationName{" ++ rn ++ "}{" ++ rn ++ "}"

showRelation :: String -> String -> String -> String
showRelation rn s t = "\\Relation{" ++ rn ++ "}{" ++ s ++ "}{" ++ t ++ "}{}"
