hets/ExtModal/ExtModal2Ship.hs

{- |
Module      :  ./ExtModal/ExtModal2Ship.hs
Description :  Translation from ExtModal to Ship
Copyright   :  (c) C. Maeder, DFKI GmbH 2012
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  Christian.Maeder@dfki.de
Stability   :  provisional
Portability :  portable
-}

module ExtModal.ExtModal2Ship where

import CASL.AS_Basic_CASL
import CASL.Fold

import ExtModal.AS_ExtModal
import ExtModal.Ship

import OWL2.AS
import OWL2.ShipSyntax
import OWL2.Translate

import Common.Id
import Common.Result

transSid :: Token -> String
transSid = transString . show

transId :: Id -> String
transId = transString . show

toFoltl :: FORMULA EM_FORMULA -> Result Foltl
toFoltl = foldFormula foltlRec

foltlRec :: Record EM_FORMULA (Result Foltl) (Result Foltl)
foltlRec = (constRecord extModalToFoltlt (const $ fail "foltlRec1")
  (fail "foltlRec2"))
  { foldQuantification = \ _ q vs f _ -> if
      q == Unique_existential then fail "Unique_existential not supported"
      else fmap (PreOp $ QuantF
        (if q == Universal then AllValuesFrom else SomeValuesFrom)
        $ concatMap (\ (Var_decl l s _) -> map
                     (\ v -> AConcept (transSid v) . CName $ transId s) l) vs)
        f
  , foldJunction = \ _ j fs _ -> fmap (JoinedF
      $ if j == Con then IntersectionOf else UnionOf) $ sequence fs
  , foldRelation = \ _ mf1 r mf2 _ -> do
       f1 <- mf1
       f2 <- mf2
       let i = BinOp f1 Impl f2
       return $ if r == Equivalence then
           JoinedF IntersectionOf [i, BinOp f2 Impl f1]
           else i
  , foldNegation = \ _ f _ -> fmap (PreOp NotF) f
  , foldAtom = \ _ b _ -> return $ if b then trueFoltl else falseFoltl
  , foldPredication = \ (Predication ps as _) _ _ _ -> case as of
    [a] -> do
      n <- toNominal a
      return . ABoxass . AConcept n . CName $ predSymToString ps
    [a1, a2] -> do
      n1 <- toNominal a1
      n2 <- toNominal a2
      return . ABoxass . ARole n1 n2 . RName $ predSymToString ps
    _ -> fail "no concept or role"
  , foldDefinedness = \ _ _ _ -> fail "foltlRec.Definedness"
  , foldEquation = \ (Equation t1 _ t2 _) _ _ _ _ -> do
      s1 <- toNominal t1
      s2 <- toNominal t2
      return . ABoxass $ AIndividual s1 Same s2
  , foldMembership = \ (Membership t s _) _ _ _ -> do
      n <- toNominal t
      return . ABoxass . AConcept n . CName $ transId s
  , foldQuantOp = \ _ _ _ _ -> fail "foltlRec.QuantOp"
  , foldQuantPred = \ _ _ _ _ -> fail "foltlRec.QuantPred"
  }

extModalToFoltlt :: EM_FORMULA -> Result Foltl
extModalToFoltlt emf = case emf of
  PrefixForm p pf _ -> do
    f <- toFoltl pf
    case p of
      NextY True -> return $ PreOp X f
      StateQuantification True b -> return $ PreOp (if b then G else F) f
      _ -> fail "extModalToFoltl.PrefixForm"
  UntilSince True f1 f2 _ -> do
    u1 <- toFoltl f1
    u2 <- toFoltl f2
    return $ BinOp u1 Until u2
  _ -> fail "extModalToFoltl"

predSymToString :: PRED_SYMB -> String
predSymToString = transId . predSymbName

toNominal :: TERM EM_FORMULA -> Result String
toNominal trm = case trm of
  Qual_var v _ _ -> return . transString $ show v
  Sorted_term t _ _ -> toNominal t
  Cast t _ _ -> toNominal t
  _ -> fail "no nominal"