{- |
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 :: TaxoGraphKind
-> MMiSSOntology
-> Sign f e
-> [Named (FORMULA f)]
-> Result MMiSSOntology
convTaxo kind :: TaxoGraphKind
kind onto :: MMiSSOntology
onto sign :: Sign f e
sign sens :: [Named (FORMULA f)]
sens =
   WithError MMiSSOntology -> Result MMiSSOntology
forall (m :: * -> *) a. MonadFail m => WithError a -> m a
fromWithError (WithError MMiSSOntology -> Result MMiSSOntology)
-> WithError MMiSSOntology -> Result MMiSSOntology
forall a b. (a -> b) -> a -> b
$
   case TaxoGraphKind
kind of
    KSubsort -> TaxoGraphKind
-> MMiSSOntology -> Sign f e -> WithError MMiSSOntology
forall f e.
TaxoGraphKind
-> MMiSSOntology -> Sign f e -> WithError MMiSSOntology
convSign TaxoGraphKind
KSubsort MMiSSOntology
onto Sign f e
sign
    KConcept -> (WithError MMiSSOntology
 -> Named (FORMULA f) -> WithError MMiSSOntology)
-> WithError MMiSSOntology
-> [Named (FORMULA f)]
-> WithError MMiSSOntology
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl WithError MMiSSOntology
-> Named (FORMULA f) -> WithError MMiSSOntology
forall f.
WithError MMiSSOntology
-> Named (FORMULA f) -> WithError MMiSSOntology
convSen (TaxoGraphKind
-> MMiSSOntology -> Sign f e -> WithError MMiSSOntology
forall f e.
TaxoGraphKind
-> MMiSSOntology -> Sign f e -> WithError MMiSSOntology
convSign TaxoGraphKind
KConcept MMiSSOntology
onto Sign f e
sign) [Named (FORMULA f)]
sens

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

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

convSen :: WithError MMiSSOntology
        -> Named (FORMULA f) -> WithError MMiSSOntology
convSen :: WithError MMiSSOntology
-> Named (FORMULA f) -> WithError MMiSSOntology
convSen weOnto :: WithError MMiSSOntology
weOnto _nSen :: Named (FORMULA f)
_nSen = (String -> WithError MMiSSOntology)
-> (MMiSSOntology -> WithError MMiSSOntology)
-> WithError MMiSSOntology
-> WithError MMiSSOntology
forall b a. (String -> b) -> (a -> b) -> WithError a -> b
weither (WithError MMiSSOntology -> String -> WithError MMiSSOntology
forall a b. a -> b -> a
const WithError MMiSSOntology
weOnto) MMiSSOntology -> WithError MMiSSOntology
forall a. a -> WithError a
hasValue WithError MMiSSOntology
weOnto

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

showRelationName :: String -> String
showRelationName :: String -> String
showRelationName rn :: String
rn = "\\RelationName{" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
rn String -> String -> String
forall a. [a] -> [a] -> [a]
++ "}{" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
rn String -> String -> String
forall a. [a] -> [a] -> [a]
++ "}"

showRelation :: String -> String -> String -> String
showRelation :: String -> String -> String -> String
showRelation rn :: String
rn s :: String
s t :: String
t = "\\Relation{" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
rn String -> String -> String
forall a. [a] -> [a] -> [a]
++ "}{" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ "}{" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
t String -> String -> String
forall a. [a] -> [a] -> [a]
++ "}{}"