content: {- |
  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
  import qualified Control.Monad.Fail as Fail
  
  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.fail "foltlRec1")
    (Fail.fail "foltlRec2"))
    { foldQuantification = \ _ q vs f _ -> if
        q == Unique_existential then Fail.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.fail "no concept or role"
    , foldDefinedness = \ _ _ _ -> Fail.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.fail "foltlRec.QuantOp"
    , foldQuantPred = \ _ _ _ _ -> Fail.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.fail "extModalToFoltl.PrefixForm"
    UntilSince True f1 f2 _ -> do
      u1 <- toFoltl f1
      u2 <- toFoltl f2
      return $ BinOp u1 Until u2
    _ -> Fail.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.fail "no nominal"
  