content: {-# LANGUAGE MultiParamTypeClasses #-}
  {-# LANGUAGE TypeSynonymInstances #-}
  {-# LANGUAGE FlexibleInstances #-}
  {- |
  Module      :  $Header$
  Description :  Comorphism from OWL 2 to CASL_Dl
  Copyright   :  (c) Francisc-Nicolae Bungiu, Felix Gabriel Mance
  License     :  GPLv2 or higher, see LICENSE.txt
  
  Maintainer  :  f.bungiu@jacobs-university.de
  Stability   :  provisional
  Portability :  non-portable (via Logic.Logic)
  -}
  
  module OWL2.OWL22CASL (OWL22CASL (..)) where
  
  import Logic.Logic as Logic
  import Logic.Comorphism
  import Common.AS_Annotation
  import Common.Result
  import Common.Id
  import Common.IRI
  import Control.Monad
  import qualified Control.Monad.Fail as Fail
  import qualified Data.Set as Set
  import qualified Data.Map as Map
  import qualified Data.List as List
  import qualified Common.Lib.MapSet as MapSet
  import qualified Common.Lib.Rel as Rel
  
  -- the DL with the initial signature for OWL
  import CASL_DL.PredefinedCASLAxioms
  
  -- OWL = domain
  import OWL2.Logic_OWL2
  import OWL2.AS as AS
  import OWL2.Parse
  import OWL2.Print
  import OWL2.ProfilesAndSublogics
  import OWL2.ManchesterPrint ()
  import OWL2.Morphism
  import OWL2.Symbols
  import qualified OWL2.Sign as OS
  import qualified OWL2.Sublogic as SL
  -- CASL_DL = codomain
  import CASL.Logic_CASL
  import CASL.AS_Basic_CASL
  import CASL.Sign
  import CASL.Morphism
  import CASL.Induction
  import CASL.Sublogic
  -- import OWL2.ManchesterParser
  
  import Common.ProofTree
  
  import Data.Maybe
  import Text.ParserCombinators.Parsec
  
  data OWL22CASL = OWL22CASL deriving Show
  
  instance Language OWL22CASL
  
  instance Comorphism
      OWL22CASL        -- comorphism
      OWL2             -- lid domain
      ProfSub          -- sublogics domain
      OntologyDocument    -- Basic spec domain
      Axiom           -- sentence domain
      SymbItems       -- symbol items domain
      SymbMapItems    -- symbol map items domain
      OS.Sign         -- signature domain
      OWLMorphism     -- morphism domain
      Entity          -- symbol domain
      RawSymb         -- rawsymbol domain
      ProofTree       -- proof tree codomain
      CASL            -- lid codomain
      CASL_Sublogics  -- sublogics codomain
      CASLBasicSpec   -- Basic spec codomain
      CASLFORMULA     -- sentence codomain
      SYMB_ITEMS      -- symbol items codomain
      SYMB_MAP_ITEMS  -- symbol map items codomain
      CASLSign        -- signature codomain
      CASLMor         -- morphism codomain
      Symbol          -- symbol codomain
      RawSymbol       -- rawsymbol codomain
      ProofTree       -- proof tree domain
      where
        sourceLogic OWL22CASL = OWL2
        sourceSublogic OWL22CASL = topS
        targetLogic OWL22CASL = CASL
        mapSublogic OWL22CASL _ = Just $ cFol
          { cons_features = emptyMapConsFeature }
        map_theory OWL22CASL = mapTheory
        map_morphism OWL22CASL = mapMorphism
        map_symbol OWL22CASL _ = mapSymbol
        isInclusionComorphism OWL22CASL = True
        has_model_expansion OWL22CASL = True
  
  -- s = emptySign ()
  
  objectPropPred :: PredType
  objectPropPred = PredType [thing, thing]
  
  dataPropPred :: PredType
  dataPropPred = PredType [thing, dataS]
  
  indiConst :: OpType
  indiConst = OpType Total [] thing
  
  
  uriToIdM :: IRI -> Result Id
  uriToIdM = return . uriToCaslId
  
  tokDecl :: Token -> VAR_DECL
  tokDecl = flip mkVarDecl thing
  
  tokDataDecl :: Token -> VAR_DECL
  tokDataDecl = flip mkVarDecl dataS
  
  nameDecl :: Int -> SORT -> VAR_DECL
  nameDecl = mkVarDecl . mkNName
  
  thingDecl :: Int -> VAR_DECL
  thingDecl = flip nameDecl thing
  
  dataDecl :: Int -> VAR_DECL
  dataDecl = flip nameDecl dataS
  
  qualThing :: Int -> TERM f
  qualThing = toQualVar . thingDecl
  
  qualData :: Int -> TERM f
  qualData = toQualVar . dataDecl
  
  implConj :: [FORMULA f] -> FORMULA f -> FORMULA f
  implConj = mkImpl . conjunct
  
  mkNC :: [FORMULA f] -> FORMULA f
  mkNC = mkNeg . conjunct
  
  mkEqVar :: VAR_DECL -> TERM f -> FORMULA f
  mkEqVar = mkStEq . toQualVar
  
  mkFEI :: [VAR_DECL] -> [VAR_DECL] -> FORMULA f -> FORMULA f -> FORMULA f
  mkFEI l1 l2 f = mkForall l1 . mkExist l2 . mkImpl f
  
  mkFIE :: [Int] -> [FORMULA f] -> Int -> Int -> FORMULA f
  mkFIE l1 l2 x y = mkVDecl l1 $ implConj l2 $ mkEqVar (thingDecl x) $ qualThing y
  
  mkFI :: [VAR_DECL] -> [VAR_DECL] -> FORMULA f -> FORMULA f -> FORMULA f
  mkFI l1 l2 f1 = (mkForall l1) . (mkImpl (mkExist l2 f1))
  
  mkRI :: [Int] -> Int -> FORMULA f -> FORMULA f
  mkRI l x so = mkVDecl l $ mkImpl (mkMember (qualThing x) thing) so
  
  mkThingVar :: VAR -> TERM f
  mkThingVar v = Qual_var v thing nullRange
  
  mkEqDecl :: Int -> TERM f -> FORMULA f
  mkEqDecl i = mkEqVar (thingDecl i)
  
  mkVDecl :: [Int] -> FORMULA f -> FORMULA f
  mkVDecl = mkForall . map thingDecl
  
  mkVDataDecl :: [Int] -> FORMULA f -> FORMULA f
  mkVDataDecl = mkForall . map dataDecl
  
  mk1VDecl :: FORMULA f -> FORMULA f
  mk1VDecl = mkVDecl [1]
  
  mkPred :: PredType -> [TERM f] -> PRED_NAME -> FORMULA f
  mkPred c tl u = mkPredication (mkQualPred u $ toPRED_TYPE c) tl
  
  mkMember :: TERM f -> SORT -> FORMULA f
  mkMember t s = Membership t s nullRange
  
  -- | Get all distinct pairs for commutative operations
  comPairs :: [t] -> [t1] -> [(t, t1)]
  comPairs [] [] = []
  comPairs _ [] = []
  comPairs [] _ = []
  comPairs (a : as) (_ : bs) = mkPairs a bs ++ comPairs as bs
  
  mkPairs :: t -> [s] -> [(t, s)]
  mkPairs a = map (\ b -> (a, b))
  
  data VarOrIndi = OVar Int | OIndi IRI
      deriving (Show, Eq, Ord)
  
  -- | Mapping of OWL morphisms to CASL morphisms
  mapMorphism :: OWLMorphism -> Result CASLMor
  mapMorphism oMor = do
        cdm <- mapSign $ osource oMor
        ccd <- mapSign $ otarget oMor
        let emap = mmaps oMor
            preds = Map.foldrWithKey (\ (Entity _ ty u1) u2 -> let
                i1 = uriToCaslId u1
                i2 = uriToCaslId u2
                in case ty of
                  Class -> Map.insert (i1, conceptPred) i2
                  ObjectProperty -> Map.insert (i1, objectPropPred) i2
                  DataProperty -> Map.insert (i1, dataPropPred) i2
                  _ -> id) Map.empty emap
            ops = Map.foldrWithKey (\ (Entity _ ty u1) u2 -> case ty of
                  NamedIndividual -> Map.insert (uriToCaslId u1, indiConst)
                    (uriToCaslId u2, Total)
                  _ -> id) Map.empty emap
        return (embedMorphism () cdm ccd)
                   { op_map = ops
                   , pred_map = preds }
  
  mapSymbol :: Entity -> Set.Set Symbol
  mapSymbol (Entity _ ty iRi) = let
    syN = Set.singleton . Symbol (uriToCaslId iRi)
    in case ty of
      Class -> syN $ PredAsItemType conceptPred
      ObjectProperty -> syN $ PredAsItemType objectPropPred
      DataProperty -> syN $ PredAsItemType dataPropPred
      NamedIndividual -> syN $ OpAsItemType indiConst
      AnnotationProperty -> Set.empty
      Datatype -> Set.empty
  
  mapSign :: OS.Sign -> Result CASLSign
  mapSign sig =
        let conc = OS.concepts sig
            cvrt = map uriToCaslId . Set.toList
            tMp k = MapSet.fromList . map (\ u -> (u, [k]))
            cPreds = thing : nothing : cvrt conc
            oPreds = cvrt $ OS.objectProperties sig
            dPreds = cvrt $ OS.dataProperties sig
            aPreds = foldr MapSet.union MapSet.empty
              [ tMp conceptPred cPreds
              , tMp objectPropPred oPreds
              , tMp dataPropPred dPreds ]
       in return $  uniteCASLSign predefSign2
           (emptySign ())
               { predMap = aPreds
               , opMap = tMp indiConst . cvrt $ OS.individuals sig
               }
  
  loadDataInformation :: ProfSub -> CASLSign
  loadDataInformation sl = let
    dts = Set.map uriToCaslId $ SL.datatype $ sublogic sl
    eSig x = (emptySign ()) { sortRel =
         Rel.fromList  [(x, dataS)]}
    sigs = Set.toList $
           Set.map (\x -> Map.findWithDefault (eSig x) x datatypeSigns) dts
   in  foldl uniteCASLSign (emptySign ()) sigs
  
  mapTheory :: (OS.Sign, [Named Axiom]) -> Result (CASLSign, [Named CASLFORMULA])
  mapTheory (owlSig, owlSens) = let
    sl = sublogicOfTheo OWL2 (owlSig, map sentence owlSens)
   in do
      cSig <- mapSign owlSig
      let pSig = loadDataInformation sl
          {- dTypes = (emptySign ()) {sortRel = Rel.transClosure . Rel.fromSet
                      . Set.map (\ d -> (uriToCaslId d, dataS))
                      . Set.union predefIRIs $ OS.datatypes owlSig} -}
      (cSens, nSigs) <- foldM (\ (x, y) z -> do
              (sen, y') <- mapSentence z
              return (sen ++ x, y ++ y')) -- uniteCASLSign sig y)) 
                       ([], []) owlSens
      return (foldl1 uniteCASLSign $ [cSig,pSig] ++ nSigs,  -- , dTypes],
              predefinedAxioms ++ (reverse cSens))
  
  -- | mapping of OWL to CASL_DL formulae
  mapSentence :: Named Axiom -> Result ([Named CASLFORMULA], [CASLSign])
  mapSentence inSen = do
      (outAx, outSigs) <- mapAxioms $ sentence inSen
      return (map (flip mapNamed inSen . const) outAx, outSigs)
  
  mapVar :: VarOrIndi -> Result (TERM ())
  mapVar v = case v of
      OVar n -> return $ qualThing n
      OIndi i -> mapIndivURI i
  
  -- | Mapping of Class URIs
  mapClassURI :: Class -> Token -> Result CASLFORMULA
  mapClassURI c t = fmap (mkPred conceptPred [mkThingVar t]) $ uriToIdM c
  
  -- | Mapping of Individual URIs
  mapIndivURI :: Individual -> Result (TERM ())
  mapIndivURI uriI = do
      ur <- uriToIdM uriI
      return $ mkAppl (mkQualOp ur (Op_type Total [] thing nullRange)) []
  
  mapNNInt :: NNInt -> TERM ()
  mapNNInt int = let NNInt uInt = int in foldr1 joinDigits $ map mkDigit uInt
  
  mapIntLit :: IntLit -> TERM ()
  mapIntLit int =
      let cInt = mapNNInt $ absInt int
      in if isNegInt int then negateInt $ upcast cInt integer
          else upcast cInt integer
  
  mapDecLit :: DecLit -> TERM ()
  mapDecLit dec =
      let ip = truncDec dec
          np = absInt ip
          fp = fracDec dec
          n = mkDecimal (mapNNInt np) (mapNNInt fp)
      in if isNegInt ip then negateFloat n else n
  
  mapFloatLit :: FloatLit -> TERM ()
  mapFloatLit f =
      let fb = floatBase f
          ex = floatExp f
       in mkFloat (mapDecLit fb) (mapIntLit ex)
  
  mapNrLit :: Literal -> TERM ()
  mapNrLit l = case l of
      NumberLit f
          | isFloatInt f -> mapIntLit $ truncDec $ floatBase f
          | isFloatDec f -> mapDecLit $ floatBase f
          | otherwise -> mapFloatLit f
      _ -> error "not number literal"
  
  mapLiteral :: Literal -> Result (TERM ())
  mapLiteral lit = return $ case lit of
      Literal l ty -> Sorted_term (case ty of
          Untyped _ -> foldr consChar emptyStringTerm l
          Typed dt -> case getDatatypeCat dt of
              OWL2Number -> let p = parse literal "" l in case p of
                  Right nr -> mapNrLit nr
                  _ -> error "cannot parse number literal"
              OWL2Bool -> case l of
                  "true" -> trueT
                  _ -> falseT
              _ -> foldr consChar emptyStringTerm l) dataS nullRange
      _ -> mapNrLit lit
  
  -- | Mapping of data properties
  mapDataProp :: DataPropertyExpression -> Int -> Int
              -> Result CASLFORMULA
  mapDataProp dp a b = fmap (mkPred dataPropPred [qualThing a, qualData b])
      $ uriToIdM dp
  
  -- | Mapping of obj props
  mapObjProp :: ObjectPropertyExpression -> Int -> Int
          -> Result CASLFORMULA
  mapObjProp ob a b = case ob of
        ObjectProp u -> fmap (mkPred objectPropPred $ map qualThing [a, b])
              $ uriToIdM u
        ObjectInverseOf u -> mapObjProp u b a
  
  -- | Mapping of obj props with Individuals
  mapObjPropI :: ObjectPropertyExpression -> VarOrIndi -> VarOrIndi
                -> Result CASLFORMULA
  mapObjPropI ob lP rP = case ob of
      ObjectProp u -> do
          l <- mapVar lP
          r <- mapVar rP
          fmap (mkPred objectPropPred [l, r]) $ uriToIdM u
      ObjectInverseOf u -> mapObjPropI u rP lP
  
  -- | mapping of individual list
  mapComIndivList :: SameOrDifferent -> Maybe Individual
      -> [Individual] -> Result [CASLFORMULA]
  mapComIndivList sod mol inds = do
      fs <- mapM mapIndivURI inds
      tps <- case mol of
          Nothing -> return $ comPairs fs fs
          Just ol -> do
              f <- mapIndivURI ol
              return $ mkPairs f fs
      return $ map (\ (x, y) -> case sod of
          Same -> mkStEq x y
          Different -> mkNeg $ mkStEq x y) tps
  
  {- | Mapping along DataPropsList for creation of pairs for commutative
  operations. -}
  mapComDataPropsList :: Maybe DataPropertyExpression
      -> [DataPropertyExpression] -> Int -> Int
      -> Result [(CASLFORMULA, CASLFORMULA)]
  mapComDataPropsList md props a b = do
      fs <- mapM (\ x -> mapDataProp x a b) props
      case md of
          Nothing -> return $ comPairs fs fs
          Just dp -> fmap (`mkPairs` fs) $ mapDataProp dp a b
  
  {- | Mapping along ObjectPropsList for creation of pairs for commutative
  operations. -}
  mapComObjectPropsList :: Maybe ObjectPropertyExpression
      -> [ObjectPropertyExpression] -> Int -> Int
      -> Result [(CASLFORMULA, CASLFORMULA)]
  mapComObjectPropsList mol props a b = do
      fs <- mapM (\ x -> mapObjProp x a b) props
      case mol of
          Nothing -> return $ comPairs fs fs
          Just ol -> fmap (`mkPairs` fs) $ mapObjProp ol a b
  
  mapDataRangeAux :: DataRange -> CASLTERM -> Result (CASLFORMULA, [CASLSign])
  mapDataRangeAux dr i = case dr of
      DataType d fl -> do
          let dt = mkMember i $ uriToCaslId d 
          (sens, s) <- mapAndUnzipM (mapFacet i) fl
          return (conjunct $ dt : sens, concat s)
      DataComplementOf drc -> do
          (sens, s) <- mapDataRangeAux drc i
          return (mkNeg sens, s)
      DataJunction jt drl -> do
          (jl, sl) <- mapAndUnzipM ((\ v r -> mapDataRangeAux r v) i) drl
          --let usig = uniteL sl
          return $ case jt of
                  IntersectionOf -> (conjunct jl, concat sl)
                  UnionOf -> (disjunct jl, concat sl)
      DataOneOf cs -> do
          ls <- mapM mapLiteral cs
          return (disjunct $ map (mkStEq i) ls, [])
  
  -- | mapping of Data Range
  mapDataRange :: DataRange -> Int -> Result (CASLFORMULA, [CASLSign])
  mapDataRange dr = mapDataRangeAux dr . qualData
  
  mkFacetPred :: TERM f -> ConstrainingFacet -> TERM f -> (FORMULA f, Id)
  mkFacetPred lit f var =
      let cf = mkInfix $ fromCF f
      in (mkPred dataPred [var, lit] cf, cf)
  
  mapFacet :: CASLTERM -> (ConstrainingFacet, RestrictionValue)
      -> Result (CASLFORMULA, [CASLSign])
  mapFacet var (f, r) = do
      con <- mapLiteral r
      let (fp, cf) = mkFacetPred con f var
      return (fp, 
              [(emptySign ()) {predMap = MapSet.fromList [(cf, [dataPred])]}])
  
  cardProps :: Bool
      -> Either ObjectPropertyExpression DataPropertyExpression -> Int
      -> [Int] -> Result [CASLFORMULA]
  cardProps b prop var vLst =
      if b then let Left ope = prop in mapM (mapObjProp ope var) vLst
       else let Right dpe = prop in mapM (mapDataProp dpe var) vLst
  
  mapCard :: Bool -> CardinalityType -> Int
      -> Either ObjectPropertyExpression DataPropertyExpression
      -> Maybe (Either ClassExpression DataRange) -> Int
      -> Result (FORMULA (), [CASLSign])
  mapCard b ct n prop d var = do
      let vlst = map (var +) [1 .. n]
          vlstM = vlst ++ [n + var + 1]
          vlstE = [n + var + 1]
      (dOut, s) <- case d of
          Nothing -> return ([], [])
          Just y ->
             if b then let Left ce = y in mapAndUnzipM
                          (mapDescription ce) vlst
             else let Right dr = y in mapAndUnzipM (mapDataRange dr) vlst
      (eOut, s') <- case d of
          Nothing -> return ([], [])
          Just y ->
             if b then let Left ce = y in mapAndUnzipM
                          (mapDescription ce) vlstM
             else let Right dr = y in mapAndUnzipM (mapDataRange dr) vlstM
      (fOut, s'') <- case d of
          Nothing -> return ([], [])
          Just y ->
             if b then let Left ce = y in mapAndUnzipM
                          (mapDescription ce) vlstE
             else let Right dr = y in mapAndUnzipM (mapDataRange dr) vlstE
      let dlst = map (\ (x, y) -> mkNeg $ mkStEq (qualThing x) $ qualThing y)
                          $ comPairs vlst vlst
          dlstM = map (\ (x, y) -> mkStEq (qualThing x) $ qualThing y)
                          $ comPairs vlstM vlstM
          qVars = map thingDecl vlst
          qVarsM = map thingDecl vlstM
          qVarsE = map thingDecl vlstE
      oProps <- cardProps b prop var vlst
      oPropsM <- cardProps b prop var vlstM
      oPropsE <- cardProps b prop var vlstE
      let minLst = conjunct $ dlst ++ oProps ++ dOut
          maxLst = mkImpl (conjunct $ oPropsM ++ eOut)
                          $ disjunct dlstM
          exactLst' = mkImpl (conjunct $ oPropsE ++ fOut) $ disjunct dlstM
          senAux = conjunct [minLst, mkForall qVarsE exactLst']
          exactLst =  if null qVars then senAux else mkExist qVars senAux
          ts = concat $ s ++ s' ++ s''
      return $ case ct of
              MinCardinality -> (mkExist qVars minLst, ts)
              MaxCardinality -> (mkForall qVarsM maxLst, ts)
              ExactCardinality -> (exactLst, ts)
  
  -- | mapping of OWL2 Descriptions
  mapDescription :: ClassExpression -> Int ->
      Result (CASLFORMULA, [CASLSign])
  mapDescription desc var = case desc of
      Expression u -> do
          c <- mapClassURI u $ mkNName var
          return (c, [])
      ObjectJunction ty ds -> do
          (els, s) <- mapAndUnzipM (flip mapDescription var) ds
          return ((case ty of
                  UnionOf -> disjunct
                  IntersectionOf -> conjunct)
              els, concat s)
      ObjectComplementOf d -> do
          (els, s) <- mapDescription d var
          return (mkNeg els, s)
      ObjectOneOf is -> do
          il <- mapM mapIndivURI is
          return (disjunct $ map (mkStEq $ qualThing var) il, [])
      ObjectValuesFrom ty o d -> let n = var + 1 in do
          oprop0 <- mapObjProp o var n
          (desc0, s) <- mapDescription d n
          return $ case ty of
              SomeValuesFrom -> (mkExist [thingDecl n] $ conjunct [oprop0, desc0],
                                 s)
              AllValuesFrom -> (mkVDecl [n] $ mkImpl oprop0 desc0,
                                 s)
      ObjectHasSelf o -> do
          op <- mapObjProp o var var
          return (op, [])
      ObjectHasValue o i -> do
          op <- mapObjPropI o (OVar var) (OIndi i)
          return (op, [])
      ObjectCardinality (Cardinality ct n oprop d) -> mapCard True ct n
          (Left oprop) (fmap Left d) var
      DataValuesFrom ty dpe dr -> let n = var + 1 in do
          oprop0 <- mapDataProp (head dpe) var n
          (desc0, s) <- mapDataRange dr n
          --let ts = niteCASLSign cSig s
          return $ case ty of
              SomeValuesFrom -> (mkExist [dataDecl n] $ conjunct [oprop0, desc0],
                  s)
              AllValuesFrom -> (mkVDataDecl [n] $ mkImpl oprop0 desc0, s)
      DataHasValue dpe c -> do
          con <- mapLiteral c
          return (mkPred dataPropPred [qualThing var, con]
                             $ uriToCaslId dpe, [])
      DataCardinality (Cardinality ct n dpe dr) -> mapCard False ct n
          (Right dpe) (fmap Right dr) var
  
  -- | Mapping of a list of descriptions
  mapDescriptionList :: Int -> [ClassExpression]
          -> Result ([CASLFORMULA], [CASLSign])
  mapDescriptionList n lst = do
      (els, s) <- mapAndUnzipM (uncurry $ mapDescription)
                      $ zip lst $ replicate (length lst) n
      return (els, concat s)
  
  -- | Mapping of a list of pairs of descriptions
  mapDescriptionListP :: Int -> [(ClassExpression, ClassExpression)]
                      -> Result ([(CASLFORMULA, CASLFORMULA)], [CASLSign])
  mapDescriptionListP  n lst = do
      let (l, r) = unzip lst
      ([lls, rls], s) <- mapAndUnzipM (mapDescriptionList n) [l, r]
      return (zip lls rls, concat s)
  
  mapCharact :: ObjectPropertyExpression -> Character
              -> Result CASLFORMULA
  mapCharact ope c = case c of
      Functional -> do
          so1 <- mapObjProp ope 1 2
          so2 <- mapObjProp ope 1 3
          return $ mkFIE [1, 2, 3] [so1, so2] 2 3
      InverseFunctional -> do
          so1 <- mapObjProp ope 1 3
          so2 <- mapObjProp ope 2 3
          return $ mkFIE [1, 2, 3] [so1, so2] 1 2
      Reflexive -> do
          so <- mapObjProp ope 1 1
          return $ mkRI [1] 1 so
      Irreflexive -> do
          so <- mapObjProp ope 1 1
          return $ mkRI [1] 1 $ mkNeg so
      Symmetric -> do
          so1 <- mapObjProp ope 1 2
          so2 <- mapObjProp ope 2 1
          return $ mkVDecl [1, 2] $ mkImpl so1 so2
      Asymmetric -> do
          so1 <- mapObjProp ope 1 2
          so2 <- mapObjProp ope 2 1
          return $ mkVDecl [1, 2] $ mkImpl so1 $ mkNeg so2
      Antisymmetric -> do
          so1 <- mapObjProp ope 1 2
          so2 <- mapObjProp ope 2 1
          return $ mkFIE [1, 2] [so1, so2] 1 2
      Transitive -> do
          so1 <- mapObjProp ope 1 2
          so2 <- mapObjProp ope 2 3
          so3 <- mapObjProp ope 1 3
          return $ mkVDecl [1, 2, 3] $ implConj [so1, so2] so3
  
  -- | Mapping of ObjectSubPropertyChain
  mapSubObjPropChain :: [ObjectPropertyExpression]
      -> ObjectPropertyExpression -> Result CASLFORMULA
  mapSubObjPropChain props oP = do
       let (_, vars) = unzip $ zip (oP:props) [1 ..]
       -- because we need n+1 vars for a chain of n roles
       oProps <- mapM (\ (z, x) -> mapObjProp z x (x+1)) $
                   zip props vars
       ooP <- mapObjProp oP 1 (head $ reverse vars)
       return $ mkVDecl vars $ implConj oProps ooP
  
  -- | Mapping of subobj properties
  mapSubObjProp :: ObjectPropertyExpression
      -> ObjectPropertyExpression -> Int -> Result CASLFORMULA
  mapSubObjProp e1 e2 a = do
      let b = a + 1
      l <- mapObjProp e1 a b
      r <- mapObjProp e2 a b
      return $ mkForallRange (map thingDecl [a, b]) (mkImpl l r) nullRange
  
  mkEDPairs :: [Int] -> Maybe AS.Relation -> [(FORMULA f, FORMULA f)]
      -> Result ([FORMULA f], [CASLSign])
  mkEDPairs il mr pairs = do
      let ls = map (\ (x, y) -> mkVDecl il
              $ case fromMaybe (error "expected EDRelation") mr of
                  EDRelation Equivalent -> mkEqv x y
                  EDRelation Disjoint -> mkNC [x, y]
                  _ -> error "expected EDRelation") pairs
      return (ls, [])
  
  mkEDPairs' :: [Int] -> Maybe AS.Relation -> [(FORMULA f, FORMULA f)]
      -> Result ([FORMULA f], [CASLSign])
  mkEDPairs' [i1, i2] mr pairs = do
      let ls = map (\ (x, y) -> mkVDecl [i1] $ mkVDataDecl [i2]
              $ case fromMaybe (error "expected EDRelation") mr of
                  EDRelation Equivalent -> mkEqv x y
                  EDRelation Disjoint -> mkNC [x, y]
                  _ -> error "expected EDRelation") pairs
      return (ls, [])
  mkEDPairs' _ _ _ = error "wrong call of mkEDPairs'"
  
  keyDecl :: Int -> [Int] -> [VAR_DECL]
  keyDecl h il = map thingDecl (take h il) ++ map dataDecl (drop h il)
  
  mapKey :: ClassExpression -> [FORMULA ()] -> [FORMULA ()]
      -> Int -> [Int] -> Int -> Result (FORMULA (), [CASLSign])
  mapKey ce pl npl p i h = do
      (nce, s) <- mapDescription ce 1
      (c3, _) <- mapDescription ce p
      let un = mkForall [thingDecl p] $ implConj (c3 : npl)
                  $ mkStEq (qualThing p) $ qualThing 1
      return (mkForall [thingDecl 1] $ mkImpl nce
              $ mkExist (keyDecl h i) $ conjunct $ pl ++ [un], s)
  
  -- mapAxioms :: Axiom -> Result ([CASLFORMULA], [CASLSign])
  -- mapAxioms (PlainAxiom ex fb) = case fb of
  --     ListFrameBit rel lfb -> mapListFrameBit ex rel lfb
  --     AnnFrameBit ans afb -> mapAnnFrameBit ex ans afb
  
  swrlVariableToVar :: IRI -> VAR_DECL
  swrlVariableToVar iri = (flip mkVarDecl) thing $ 
      case List.stripPrefix "urn:swrl#" (showIRI iri) of
          Nothing -> idToSimpleId . uriToCaslId $ iri
          Just var -> genToken var
  
  mapAxioms :: Axiom -> Result([CASLFORMULA], [CASLSign])
  mapAxioms axiom = case axiom of
      Declaration _ _ -> return ([], [])
  
      ClassAxiom clAxiom -> case clAxiom of
          SubClassOf _ sub sup -> do
              (domT, s1) <- mapDescription sub 1
              (codT, s2) <- mapDescriptionList 1 [sup]
              return (map (mk1VDecl . mkImpl domT) codT,
                      s1 ++ s2)
      
          EquivalentClasses _ cel -> do
              (els, _) <- mapDescriptionListP 1 $ comPairs cel cel
              mkEDPairs [1] (Just $ EDRelation Equivalent) els
  
          DisjointClasses _ cel -> do
              (els, _) <- mapDescriptionListP 1 $ comPairs cel cel
              mkEDPairs [1] (Just $ EDRelation Disjoint) els
  
          DisjointUnion _ clIri clsl -> do
              (decrs, s1) <- mapDescriptionList 1 clsl
              (decrsS, s2) <- mapDescriptionListP 1 $ comPairs clsl clsl
              let decrsP = map (\ (x, y) -> conjunct [x, y]) decrsS
              mcls <- mapClassURI clIri $ mkNName 1
              return ([mk1VDecl $ mkEqv mcls $ conjunct
                      [disjunct decrs, mkNC decrsP]], s1 ++ s2)
  
      ObjectPropertyAxiom opAxiom -> case opAxiom of
          SubObjectPropertyOf _ subOpExpr supOpExpr -> case subOpExpr of
              SubObjPropExpr_obj opExpr -> do
                  os <- mapM (\ (o1, o2) -> mapSubObjProp o1 o2 3)
                      $ mkPairs opExpr [supOpExpr]
                  return (os, [])
              SubObjPropExpr_exprchain opExprs -> do
                  os <- mapSubObjPropChain opExprs supOpExpr
                  return ([os], [])
  
          EquivalentObjectProperties _ opExprs -> do
              pairs <- mapComObjectPropsList Nothing opExprs 1 2
              mkEDPairs [1, 2] (Just $ EDRelation Equivalent) pairs
  
          DisjointObjectProperties _ opExprs -> do
              pairs <- mapComObjectPropsList Nothing opExprs 1 2
              mkEDPairs [1, 2] (Just $ EDRelation Disjoint) pairs
  
          InverseObjectProperties _ opExpr1 opExpr2 -> do
              os1 <- mapM (\o1 -> mapObjProp o1 1 2) [opExpr2]
              o2 <- mapObjProp opExpr1 2 1
              return (map (mkVDecl [1, 2] . mkEqv o2) os1, [])
  
          ObjectPropertyDomain _ opExpr clExpr -> do
              tobjP <- mapObjProp opExpr 1 2
              (tdsc, s) <- mapAndUnzipM (\c -> mapDescription c 1) [clExpr]
              let vars = (mkNName 1, mkNName 2)
              return (map (mkFI [tokDecl $ fst vars] [tokDecl $ snd vars] tobjP) tdsc,
                      concat s)
  
          ObjectPropertyRange _ opExpr clExpr -> do
              tobjP <- mapObjProp opExpr 1 2
              (tdsc, s) <- mapAndUnzipM (\c -> mapDescription c 2) [clExpr]
              let vars = (mkNName 2, mkNName 1)
              return (map (mkFI [tokDecl $ fst vars] [tokDecl $ snd vars] tobjP) tdsc,
                      concat s)
  
          FunctionalObjectProperty _ opExpr -> do
              cl <- mapM (mapCharact opExpr) [Functional]
              return (cl, [])
  
          InverseFunctionalObjectProperty _ opExpr -> do
              cl <- mapM (mapCharact opExpr) [InverseFunctional]
              return (cl, [])
              
          ReflexiveObjectProperty _ opExpr -> do
              cl <- mapM (mapCharact opExpr) [Reflexive]
              return (cl, [])
  
          IrreflexiveObjectProperty _ opExpr -> do
              cl <- mapM (mapCharact opExpr) [Irreflexive]
              return (cl, [])
  
          SymmetricObjectProperty _ opExpr -> do
              cl <- mapM (mapCharact opExpr) [Symmetric]
              return (cl, [])
  
          AsymmetricObjectProperty _ opExpr -> do
              cl <- mapM (mapCharact opExpr) [Asymmetric]
              return (cl, [])
  
          TransitiveObjectProperty _ opExpr -> do
              cl <- mapM (mapCharact opExpr) [Transitive]
              return (cl, [])
  
      DataPropertyAxiom dpAxiom -> case dpAxiom of
          SubDataPropertyOf _ subDpExpr supDpExpr -> do
              os1 <- mapM (\ o1 -> mapDataProp o1 1 2) [supDpExpr]
              o2 <- mapDataProp subDpExpr 1 2 -- was 2 1
              return (map (mkForall [thingDecl 1, dataDecl 2]
                  . mkImpl o2) os1, [])  
          
          EquivalentDataProperties _ dpExprs -> do
              pairs <- mapComDataPropsList Nothing dpExprs 1 2
              mkEDPairs' [1, 2] (Just $ EDRelation Equivalent) pairs
  
          DisjointDataProperties _ dpExprs -> do
              pairs <- mapComDataPropsList Nothing dpExprs 1 2
              mkEDPairs' [1, 2] (Just $ EDRelation Disjoint) pairs
  
          DataPropertyDomain _ dpExpr clExpr -> do
              (els, s) <- mapAndUnzipM (\ c -> mapDescription c 1) [clExpr]
              oEx <- mapDataProp dpExpr 1 2
              let vars = (mkNName 1, mkNName 2)
              return (map (mkFI [tokDecl $ fst vars]
                  [mkVarDecl (snd vars) dataS] oEx) els, concat s)
  
          DataPropertyRange _ dpExpr dr -> do
              oEx <- mapDataProp dpExpr 1 2
              (odes, s) <- mapAndUnzipM (\r -> mapDataRange r 2) [dr]
              let vars = (mkNName 1, mkNName 2)
              return (map (mkFEI [tokDecl $ fst vars]
                          [tokDataDecl $ snd vars] oEx) odes, concat s)
  
          FunctionalDataProperty _ dpExpr -> do
              so1 <- mapDataProp dpExpr 1 2
              so2 <- mapDataProp dpExpr 1 3
              return ([mkForall (thingDecl 1 : map dataDecl [2, 3]) $ implConj
                          [so1, so2] $ mkEqVar (dataDecl 2) $ qualData 3], [])
  
      DatatypeDefinition _ dt dr -> do
          (odes, s) <- mapDataRange dr 2
          return ([mkVDataDecl [2] $ mkEqv odes $ mkMember
                  (qualData 2) $ uriToCaslId dt], s)
  
      
      HasKey _ ce opl dpl -> do
          let lo = length opl 
              ld = length dpl
              uptoOP = [2 .. lo + 1]
              uptoDP = [lo + 2 .. lo + ld + 1]
              tl = lo + ld + 2
          ol <- mapM (\ (n, o) -> mapObjProp o 1 n) $ zip uptoOP opl
          nol <- mapM (\ (n, o) -> mapObjProp o tl n) $ zip uptoOP opl
          dl <- mapM (\ (n, d) -> mapDataProp d 1 n) $ zip uptoDP dpl
          ndl <- mapM (\ (n, d) -> mapDataProp d tl n) $ zip uptoDP dpl
          (keys, s) <-
              mapKey ce (ol ++ dl) (nol ++ ndl) tl (uptoOP ++ uptoDP) lo
          return ([keys], s)
  
      Assertion assertion -> case assertion of
          SameIndividual _ inds -> do
              let (mi, rest) = case inds of
                      (iri:r) -> (Just iri, r)
                      _ -> (Nothing, inds)
              fs <- mapComIndivList Same mi rest
              return (fs, [])
  
          DifferentIndividuals _ inds -> do
              let (mi, rest) = case inds of
                      (iri:r) -> (Just iri, r)
                      _ -> (Nothing, inds)
              fs <- mapComIndivList Different mi rest
              return (fs, [])
  
          ClassAssertion _ ce iIri -> do
              (els, s) <- mapAndUnzipM (\c -> mapDescription c 1) [ce]
              inD <- mapIndivURI iIri
              let els' = map (substitute (mkNName 1) thing inD) els
              return ( els', concat s)
  
          ObjectPropertyAssertion _ op si ti -> do
              oPropH <- mapObjPropI op (OIndi si) (OIndi ti)
              return ([oPropH], [])
  
          NegativeObjectPropertyAssertion _ op si ti -> do
              oPropH <- mapObjPropI op (OIndi si) (OIndi ti)
              let oProp = Negation oPropH nullRange
              return ([oProp], [])
  
          DataPropertyAssertion _ dp si tv -> do
              inS <- mapIndivURI si
              inT <- mapLiteral tv
              oProp <- mapDataProp dp 1 2
              return ([mkForall [thingDecl 1, dataDecl 2] $ implConj
                  [mkEqDecl 1 inS, mkEqVar (dataDecl 2) $ upcast inT dataS] oProp],
                  [])
  
          NegativeDataPropertyAssertion _ dp si tv -> do
              inS <- mapIndivURI si
              inT <- mapLiteral tv
              oPropH <- mapDataProp dp 1 2
              let oProp = Negation oPropH nullRange
              return ([mkForall [thingDecl 1, dataDecl 2] $ implConj
                  [mkEqDecl 1 inS, mkEqVar (dataDecl 2) $ upcast inT dataS] oProp],
                  [])
  
      AnnotationAxiom _ -> return ([], [])
  
      Rule rule -> case rule of
          DLSafeRule _ b h ->
              let vars = Set.toList . Set.unions $ getVariablesFromAtom <$> (b ++ h)
                  names = swrlVariableToVar <$> vars
                  f (s, sig, startVal) at = do
                      (sentences', sig', offsetValue) <- atomToSentence startVal at
                      return (s ++ sentences', sig ++ sig', offsetValue)
  
                  g startVal atoms = foldM f ([], [], startVal) atoms
              in do
                  (antecedentSen, sig1, offsetValue) <- g 1 b
                  let antecedent = conjunct antecedentSen
                  
                  (consequentSen, sig2, lastVar) <- g offsetValue h
                  let consequent = conjunct consequentSen
  
                  
                  let impl = mkImpl antecedent consequent
                  return $ ([mkForall (names ++ map thingDecl [1..lastVar - 1]) impl], sig1 ++ sig2)
          DGRule _ _ _ -> Fail.fail "Translating DGRules is not supported yet!"
      DGAxiom _ _ _ _ _ -> Fail.fail "Translating DGAxioms is not supported yet!"
  
  
  iArgToTerm :: IndividualArg -> Result(TERM ())
  iArgToTerm arg = case arg of
      IVar v -> return . toQualVar . swrlVariableToVar $ v
      IArg iri -> mapIndivURI iri
  
  iArgToVarOrIndi :: IndividualArg -> VarOrIndi
  iArgToVarOrIndi arg = case arg of
      IVar v -> OIndi v
      IArg iri -> OIndi iri
  
  
  iArgToIRI :: IndividualArg -> IRI
  iArgToIRI arg = case arg of
      IVar var -> var
      IArg ind -> ind
  
  
  dArgToTerm :: DataArg -> Result (TERM ())
  dArgToTerm arg = case arg of
      DVar var -> return . toQualVar .  tokDataDecl . uriToTok $ var
      DArg lit -> mapLiteral lit
  
  atomToSentence :: Int -> Atom -> Result ([CASLFORMULA], [CASLSign], Int)
  atomToSentence startVar atom = case atom of
      ClassAtom clExpr iarg -> do 
          (el, sigs) <- mapDescription clExpr startVar
          inD <- iArgToTerm iarg
          let el' = substitute (mkNName startVar) thing inD el
          return ([el'], sigs, startVar)
          
      DataRangeAtom dr darg -> do
          dt <- dArgToTerm darg
          (odes, s) <- mapDataRangeAux dr dt
          return ([substitute (mkNName 1) thing dt odes], s, startVar)
  
      ObjectPropertyAtom opExpr iarg1 iarg2 -> do
          let si = iArgToVarOrIndi iarg1
              ti = iArgToVarOrIndi iarg2
          oPropH <- mapObjPropI opExpr si ti
          return ([oPropH], [], startVar)
  
      DataPropertyAtom dpExpr iarg darg -> do
          let a = 1
              b = 2
          inS <- iArgToTerm iarg
          inT <- dArgToTerm darg
          oProp <- mapDataProp dpExpr a b
          return ([mkForall [thingDecl a, dataDecl b] $ implConj
              [mkEqDecl a inS, mkEqVar (dataDecl b) $ upcast inT dataS] oProp],
              [], startVar)
  
      BuiltInAtom iri args -> do
          prdArgs <- mapM dArgToTerm args
          let predtype = PredType $ map (const thing) args
              prd = mkPred predtype prdArgs (uriToId iri)
  
          return ([prd], [], startVar)
  
      SameIndividualAtom iarg1 iarg2 -> do
              fs <- mapComIndivList Same (Just $ iArgToIRI iarg1) [iArgToIRI iarg2]
              return (fs, [], startVar)
          
      DifferentIndividualsAtom iarg1 iarg2 -> do
              fs <- mapComIndivList Different (Just $ iArgToIRI iarg1) [iArgToIRI iarg2]
              return (fs, [], startVar)
      _ -> Fail.fail $ "Couldn't translate unknown atom '" ++ show atom ++ "'!"
  