content: {-# LANGUAGE DeriveDataTypeable #-}
  {- |
  Module      :  ./CASL_DL/Sign.hs
  Description :  Signatures for DL logics, as extension of CASL signatures
  Copyright   :  (c) Klaus Luettich, Uni Bremen 2004
  License     :  GPLv2 or higher, see LICENSE.txt
  
  Maintainer  :  luecke@informatik.uni-bremen.de
  Stability   :  provisional
  Portability :  portable
  
  Signatures for DL logics, as extension of CASL signatures.
  -}
  
  module CASL_DL.Sign where
  
  import Data.Data
  import qualified Data.Map as Map
  
  import Common.Id
  import Common.Doc
  import Common.DocUtils
  
  import CASL.AS_Basic_CASL
  import CASL_DL.AS_CASL_DL
  import CASL_DL.Print_AS ()
  
  import Data.List (union, (\\), isPrefixOf)
  import Control.Exception
  
  data CASL_DLSign =
      CASL_DLSign { annoProperties :: Map.Map SIMPLE_ID PropertyType
                  , annoPropertySens :: [AnnoAppl]
                  } deriving (Show, Eq, Ord, Typeable, Data)
  
  data PropertyType = AnnoProperty
                    | OntoProperty deriving (Show, Eq, Ord, Typeable, Data)
  
  data AnnoAppl = AnnoAppl SIMPLE_ID Id AnnoLiteral
                  deriving (Show, Eq, Ord, Typeable, Data)
  
  data AnnoLiteral = AL_Term (TERM DL_FORMULA)
                   | AL_Id Id
                     deriving (Show, Eq, Ord, Typeable, Data)
  
  emptyCASL_DLSign :: CASL_DLSign
  emptyCASL_DLSign = CASL_DLSign Map.empty []
  
  addCASL_DLSign :: CASL_DLSign -> CASL_DLSign -> CASL_DLSign
  addCASL_DLSign a b = a
       { annoProperties =
             Map.unionWithKey (throwAnnoError "CASL_DL.Sign.addCASL_DLSign:")
                    (annoProperties a) (annoProperties b)
       , annoPropertySens = union (annoPropertySens a) (annoPropertySens b)
       }
  
  throwAnnoError :: String -> SIMPLE_ID
                 -> PropertyType -> PropertyType -> PropertyType
  throwAnnoError s k e1 e2 =
      if e1 == e2
         then e1
         else error $ s ++ " Annotation Properties and Ontology Properties "
                  ++ "must have distinct names! (" ++ show k ++ ")"
  
  diffCASL_DLSign :: CASL_DLSign -> CASL_DLSign -> CASL_DLSign
  diffCASL_DLSign a b = a
       { annoProperties = Map.difference (annoProperties a) (annoProperties b)
       , annoPropertySens = annoPropertySens a \\ annoPropertySens b
       }
  
  isSubCASL_DLSign :: CASL_DLSign -> CASL_DLSign -> Bool
  isSubCASL_DLSign a b =
      Map.isSubmapOf (annoProperties a) (annoProperties b) &&
      (annoPropertySens a `isSublistOf` annoPropertySens b)
  
  instance Pretty CASL_DLSign where
      pretty dlSign = if Map.null $ annoProperties dlSign
                      then assert (null $ annoPropertySens dlSign) empty
                      else printPropertyList AnnoProperty
                                             "%OWLAnnoProperties("
                           $+$
                           printPropertyList OntoProperty
                                             "%OWLOntologyProperties("
                           $+$
                           if null (annoPropertySens dlSign)
                           then empty
                           else text "%OWLAnnotations(" <+>
                                vcat (punctuate (text "; ") $
                                      map pretty
                                       (annoPropertySens dlSign)) <+>
                                text ")%"
          where propertyList ty = filter (\ (_, x) -> x == ty) $
                                   Map.toList $ annoProperties dlSign
                printPropertyList ty str =
                    case propertyList ty of
                      [] -> empty
                      l -> text str <+>
                            fcat (punctuate comma $
                                  map (pretty . fst) l) <+>
                            text ")%"
  
  
  instance Pretty AnnoAppl where
      pretty (AnnoAppl rel subj obj) = pretty rel <>
                                       parens (pretty subj <> comma <> pretty obj)
  
  instance Pretty AnnoLiteral where
      pretty annoLit = case annoLit of
                         AL_Term t -> pretty t
                         AL_Id i -> pretty i
  
  isSublistOf :: (Eq a) => [a] -> [a] -> Bool
  isSublistOf ys l = case l of
    [] -> null ys
    _ : l' -> isPrefixOf ys l || isSublistOf ys l'
  