{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, 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 Control.Monad
import Data.Char
import qualified Data.Set as Set
import qualified Data.Map as Map
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.Keywords
import OWL2.MS
import OWL2.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
-- CASL_DL = codomain
import CASL.Logic_CASL
import CASL.AS_Basic_CASL
import CASL.Sign
import CASL.Morphism
import CASL.Sublogic
-- import OWL2.ManchesterParser

import Common.ProofTree
import Common.DocUtils

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 ()

uniteL :: [CASLSign] -> CASLSign
uniteL = foldl1 uniteCASLSign

failMsg :: Pretty a => a -> Result b
failMsg a = fail $ "cannot translate " ++ showDoc a "\n"

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

-- | Extracts Id from URI
uriToCaslId :: IRI -> Id
uriToCaslId urI =
    let l = localPart urI
        ur = if isThing urI then mkQName l else urI
        repl a = if isAlphaNum a then [a] else "_u"
        nP = concatMap repl $ namePrefix ur
        lP = concatMap repl l
    in stringToId $ (if isDatatypeKey urI then "" else nP) ++ lP

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

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.foldWithKey (\ (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.foldWithKey (\ (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 predefSign (emptySign ())
             { predMap = aPreds
             , opMap = tMp indiConst . cvrt $ OS.individuals sig
             }

loadDataInformation :: ProfSub -> Sign f ()
loadDataInformation _ = let dts = Set.fromList $ map stringToId datatypeKeys
    in (emptySign ()) { sortRel = Rel.fromKeysSet dts }

mapTheory :: (OS.Sign, [Named Axiom]) -> Result (CASLSign, [Named CASLFORMULA])
mapTheory (owlSig, owlSens) = let sl = topS in do
    cSig <- mapSign owlSig
    let pSig = loadDataInformation sl
        dTypes = (emptySign ()) {sortRel = Rel.transClosure $ Rel.fromList
                    $ map (\ d -> (uriToCaslId d, dataS))
                    $ predefIRIs ++ Set.toList (OS.datatypes owlSig)}
    (cSens, nSig) <- foldM (\ (x, y) z -> do
            (sen, sig) <- mapSentence y z
            return (sen ++ x, uniteCASLSign sig y)) ([], cSig) owlSens
    return (foldl1 uniteCASLSign [nSig, pSig, dTypes],
                predefinedAxioms ++ cSens)

-- | mapping of OWL to CASL_DL formulae
mapSentence :: CASLSign -> Named Axiom -> Result ([Named CASLFORMULA], CASLSign)
mapSentence cSig inSen = do
    (outAx, outSig) <- mapAxioms cSig $ sentence inSen
    return (map (flip mapNamed inSen . const) outAx, outSig)

mapVar :: CASLSign -> VarOrIndi -> Result (TERM ())
mapVar cSig v = case v of
    OVar n -> return $ qualThing n
    OIndi i -> mapIndivURI cSig i

-- | Mapping of Class URIs
mapClassURI :: CASLSign -> Class -> Token -> Result CASLFORMULA
mapClassURI _ c t = fmap (mkPred conceptPred [mkThingVar t]) $ uriToIdM c

-- | Mapping of Individual URIs
mapIndivURI :: CASLSign -> 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 :: CASLSign -> DataPropertyExpression -> Int -> Int
            -> Result CASLFORMULA
mapDataProp _ dp a b = fmap (mkPred dataPropPred [qualThing a, qualData b])
    $ uriToIdM dp

-- | Mapping of obj props
mapObjProp :: CASLSign -> ObjectPropertyExpression -> Int -> Int
        -> Result CASLFORMULA
mapObjProp cSig ob a b = case ob of
      ObjectProp u -> fmap (mkPred objectPropPred $ map qualThing [a, b])
            $ uriToIdM u
      ObjectInverseOf u -> mapObjProp cSig u b a

-- | Mapping of obj props with Individuals
mapObjPropI :: CASLSign -> ObjectPropertyExpression -> VarOrIndi -> VarOrIndi
              -> Result CASLFORMULA
mapObjPropI cSig ob lP rP = case ob of
    ObjectProp u -> do
        l <- mapVar cSig lP
        r <- mapVar cSig rP
        fmap (mkPred objectPropPred [l, r]) $ uriToIdM u
    ObjectInverseOf u -> mapObjPropI cSig u rP lP

-- | mapping of individual list
mapComIndivList :: CASLSign -> SameOrDifferent -> Maybe Individual
    -> [Individual] -> Result [CASLFORMULA]
mapComIndivList cSig sod mol inds = do
    fs <- mapM (mapIndivURI cSig) inds
    tps <- case mol of
        Nothing -> return $ comPairs fs fs
        Just ol -> do
            f <- mapIndivURI cSig 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 :: CASLSign -> Maybe DataPropertyExpression
    -> [DataPropertyExpression] -> Int -> Int
    -> Result [(CASLFORMULA, CASLFORMULA)]
mapComDataPropsList cSig md props a b = do
    fs <- mapM (\ x -> mapDataProp cSig x a b) props
    case md of
        Nothing -> return $ comPairs fs fs
        Just dp -> fmap (`mkPairs` fs) $ mapDataProp cSig dp a b

{- | Mapping along ObjectPropsList for creation of pairs for commutative
operations. -}
mapComObjectPropsList :: CASLSign -> Maybe ObjectPropertyExpression
    -> [ObjectPropertyExpression] -> Int -> Int
    -> Result [(CASLFORMULA, CASLFORMULA)]
mapComObjectPropsList cSig mol props a b = do
    fs <- mapM (\ x -> mapObjProp cSig x a b) props
    case mol of
        Nothing -> return $ comPairs fs fs
        Just ol -> fmap (`mkPairs` fs) $ mapObjProp cSig ol a b

-- | mapping of Data Range
mapDataRange :: CASLSign -> DataRange -> Int -> Result (CASLFORMULA, CASLSign)
mapDataRange cSig dr i = case dr of
    DataType d fl -> do
        let dt = mkMember (qualData i) $ uriToCaslId d
        (sens, s) <- mapAndUnzipM (mapFacet cSig i) fl
        return (conjunct $ dt : sens, uniteL $ cSig : s)
    DataComplementOf drc -> do
        (sens, s) <- mapDataRange cSig drc i
        return (mkNeg sens, uniteCASLSign cSig s)
    DataJunction jt drl -> do
        (jl, sl) <- mapAndUnzipM ((\ s v r -> mapDataRange s r v) cSig i) drl
        let usig = uniteL sl
        return $ case jt of
                IntersectionOf -> (conjunct jl, usig)
                UnionOf -> (disjunct jl, usig)
    DataOneOf cs -> do
        ls <- mapM mapLiteral cs
        return (disjunct $ map (mkStEq $ qualData i) ls, cSig)

mkFacetPred :: TERM f -> ConstrainingFacet -> Int -> (FORMULA f, Id)
mkFacetPred lit f var =
    let cf = mkInfix $ fromCF f
    in (mkPred dataPred [qualData var, lit] cf, cf)

mapFacet :: CASLSign -> Int -> (ConstrainingFacet, RestrictionValue)
    -> Result (CASLFORMULA, CASLSign)
mapFacet sig var (f, r) = do
    con <- mapLiteral r
    let (fp, cf) = mkFacetPred con f var
    return (fp, uniteCASLSign sig $ (emptySign ())
            {predMap = MapSet.fromList [(cf, [dataPred])]})

cardProps :: Bool -> CASLSign
    -> Either ObjectPropertyExpression DataPropertyExpression -> Int
    -> [Int] -> Result [CASLFORMULA]
cardProps b cSig prop var vLst =
    if b then let Left ope = prop in mapM (mapObjProp cSig ope var) vLst
     else let Right dpe = prop in mapM (mapDataProp cSig dpe var) vLst

mapCard :: Bool -> CASLSign -> CardinalityType -> Int
    -> Either ObjectPropertyExpression DataPropertyExpression
    -> Maybe (Either ClassExpression DataRange) -> Int
    -> Result (FORMULA (), CASLSign)
mapCard b cSig ct n prop d var = do
    let vlst = map (var +) [1 .. n]
        vlstM = vlst ++ [n + var + 1]
    (dOut, s) <- case d of
        Nothing -> return ([], [emptySign ()])
        Just y ->
           if b then let Left ce = y in mapAndUnzipM
                        (mapDescription cSig ce) vlst
           else let Right dr = y in mapAndUnzipM (mapDataRange cSig dr) vlst
    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
    oProps <- cardProps b cSig prop var vlst
    oPropsM <- cardProps b cSig prop var vlstM
    let minLst = mkExist qVars $ conjunct $ dlst ++ dOut ++ oProps
        maxLst = mkForall qVarsM $ mkImpl (conjunct $ oPropsM ++ dOut)
                        $ disjunct dlstM
        ts = uniteL $ cSig : s
    return $ case ct of
            MinCardinality -> (minLst, ts)
            MaxCardinality -> (maxLst, ts)
            ExactCardinality -> (conjunct [minLst, maxLst], ts)

-- | mapping of OWL2 Descriptions
mapDescription :: CASLSign -> ClassExpression -> Int ->
    Result (CASLFORMULA, CASLSign)
mapDescription cSig desc var = case desc of
    Expression u -> do
        c <- mapClassURI cSig u $ mkNName var
        return (c, cSig)
    ObjectJunction ty ds -> do
        (els, s) <- mapAndUnzipM (flip (mapDescription cSig) var) ds
        return ((case ty of
                UnionOf -> disjunct
                IntersectionOf -> conjunct)
            els, uniteL $ cSig : s)
    ObjectComplementOf d -> do
        (els, s) <- mapDescription cSig d var
        return (mkNeg els, uniteCASLSign cSig s)
    ObjectOneOf is -> do
        il <- mapM (mapIndivURI cSig) is
        return (disjunct $ map (mkStEq $ qualThing var) il, cSig)
    ObjectValuesFrom ty o d -> let n = var + 1 in do
        oprop0 <- mapObjProp cSig o var n
        (desc0, s) <- mapDescription cSig d n
        return $ case ty of
            SomeValuesFrom -> (mkExist [thingDecl n] $ conjunct [oprop0, desc0],
                    uniteCASLSign cSig s)
            AllValuesFrom -> (mkVDecl [n] $ mkImpl oprop0 desc0,
                    uniteCASLSign cSig s)
    ObjectHasSelf o -> do
        op <- mapObjProp cSig o var var
        return (op, cSig)
    ObjectHasValue o i -> do
        op <- mapObjPropI cSig o (OVar var) (OIndi i)
        return (op, cSig)
    ObjectCardinality (Cardinality ct n oprop d) -> mapCard True cSig ct n
        (Left oprop) (fmap Left d) var
    DataValuesFrom ty dpe dr -> let n = var + 1 in do
        oprop0 <- mapDataProp cSig dpe var n
        (desc0, s) <- mapDataRange cSig dr n
        let ts = uniteCASLSign cSig s
        return $ case ty of
            SomeValuesFrom -> (mkExist [dataDecl n] $ conjunct [oprop0, desc0],
                ts)
            AllValuesFrom -> (mkVDataDecl [n] $ mkImpl oprop0 desc0, ts)
    DataHasValue dpe c -> do
        con <- mapLiteral c
        return (mkPred dataPropPred [qualThing var, con]
                           $ uriToCaslId dpe, cSig)
    DataCardinality (Cardinality ct n dpe dr) -> mapCard False cSig ct n
        (Right dpe) (fmap Right dr) var

-- | Mapping of a list of descriptions
mapDescriptionList :: CASLSign -> Int -> [ClassExpression]
        -> Result ([CASLFORMULA], CASLSign)
mapDescriptionList cSig n lst = do
    (els, s) <- mapAndUnzipM (uncurry $ mapDescription cSig)
                    $ zip lst $ replicate (length lst) n
    return (els, uniteL $ cSig : s)

-- | Mapping of a list of pairs of descriptions
mapDescriptionListP :: CASLSign -> Int -> [(ClassExpression, ClassExpression)]
                    -> Result ([(CASLFORMULA, CASLFORMULA)], CASLSign)
mapDescriptionListP cSig n lst = do
    let (l, r) = unzip lst
    ([lls, rls], s) <- mapAndUnzipM (mapDescriptionList cSig n) [l, r]
    return (zip lls rls, uniteL $ cSig : s)

mapFact :: CASLSign -> Extended -> Fact -> Result CASLFORMULA
mapFact cSig ex f = case f of
    ObjectPropertyFact posneg obe ind -> case ex of
        SimpleEntity (Entity NamedIndividual siri) -> do
            inS <- mapIndivURI cSig siri
            inT <- mapIndivURI cSig ind
            oPropH <- mapObjProp cSig obe 1 2
            let oProp = case posneg of
                    Positive -> oPropH
                    Negative -> Negation oPropH nullRange
            return $ mkVDecl [1, 2] $ implConj
                            [mkEqDecl 1 inS, mkEqDecl 2 inT] oProp
        _ -> fail $ "ObjectPropertyFactsFacts Entity fail: " ++ show f
    DataPropertyFact posneg dpe lit -> case ex of
        SimpleEntity (Entity NamedIndividual iri) -> do
            inS <- mapIndivURI cSig iri
            inT <- mapLiteral lit
            oPropH <- mapDataProp cSig dpe 1 2
            let oProp = case posneg of
                    Positive -> oPropH
                    Negative -> Negation oPropH nullRange
            return $ mkForall [thingDecl 1, dataDecl 2] $ implConj
                [mkEqDecl 1 inS, mkEqVar (dataDecl 2) $ upcast inT dataS] oProp
        _ -> fail $ "DataPropertyFact Entity fail " ++ show f

mapCharact :: CASLSign -> ObjectPropertyExpression -> Character
            -> Result CASLFORMULA
mapCharact cSig ope c = case c of
    Functional -> do
        so1 <- mapObjProp cSig ope 1 2
        so2 <- mapObjProp cSig ope 1 3
        return $ mkFIE [1, 2, 3] [so1, so2] 2 3
    InverseFunctional -> do
        so1 <- mapObjProp cSig ope 1 3
        so2 <- mapObjProp cSig ope 2 3
        return $ mkFIE [1, 2, 3] [so1, so2] 1 2
    Reflexive -> do
        so <- mapObjProp cSig ope 1 1
        return $ mkRI [1] 1 so
    Irreflexive -> do
        so <- mapObjProp cSig ope 1 1
        return $ mkRI [1] 1 $ mkNeg so
    Symmetric -> do
        so1 <- mapObjProp cSig ope 1 2
        so2 <- mapObjProp cSig ope 2 1
        return $ mkVDecl [1, 2] $ mkImpl so1 so2
    Asymmetric -> do
        so1 <- mapObjProp cSig ope 1 2
        so2 <- mapObjProp cSig ope 2 1
        return $ mkVDecl [1, 2] $ mkImpl so1 $ mkNeg so2
    Antisymmetric -> do
        so1 <- mapObjProp cSig ope 1 2
        so2 <- mapObjProp cSig ope 2 1
        return $ mkFIE [1, 2] [so1, so2] 1 2
    Transitive -> do
        so1 <- mapObjProp cSig ope 1 2
        so2 <- mapObjProp cSig ope 2 3
        so3 <- mapObjProp cSig ope 1 3
        return $ mkVDecl [1, 2, 3] $ implConj [so1, so2] so3

-- | Mapping of ObjectSubPropertyChain
mapSubObjPropChain :: CASLSign -> [ObjectPropertyExpression]
    -> ObjectPropertyExpression -> Int -> Result CASLFORMULA
mapSubObjPropChain cSig props oP n = let m = n + 1 in do
    let (_, vars) = unzip $ zip (tail props) [m + 1 ..]
        vl = n : vars ++ [m]
    oProps <- mapM (\ (z, x, y) -> mapObjProp cSig z x y) $
                zip3 props vl $ tail vl
    ooP <- mapObjProp cSig oP n m
    return $ mkVDecl [1, 2] $ mkVDecl vars $ implConj oProps ooP

-- | Mapping of subobj properties
mapSubObjProp :: CASLSign -> ObjectPropertyExpression
    -> ObjectPropertyExpression -> Int -> Result CASLFORMULA
mapSubObjProp cSig e1 e2 a = do
    let b = a + 1
    l <- mapObjProp cSig e1 a b
    r <- mapObjProp cSig e2 a b
    return $ mkForallRange (map thingDecl [a, b]) (mkImpl l r) nullRange

mkEDPairs :: CASLSign -> [Int] -> Maybe Relation -> [(FORMULA f, FORMULA f)]
    -> Result ([FORMULA f], CASLSign)
mkEDPairs s 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, s)

-- | Mapping of ListFrameBit
mapListFrameBit :: CASLSign -> Extended -> Maybe Relation -> ListFrameBit
       -> Result ([CASLFORMULA], CASLSign)
mapListFrameBit cSig ex rel lfb = case lfb of
    AnnotationBit _ -> return ([], cSig)
    ExpressionBit cls -> case ex of
          Misc _ -> let cel = map snd cls in do
            (els, s) <- mapDescriptionListP cSig 1 $ comPairs cel cel
            mkEDPairs (uniteCASLSign cSig s) [1] rel els
          SimpleEntity (Entity ty iri) -> do
              (els, s) <- mapAndUnzipM (\ (_, c) -> mapDescription cSig c 1) cls
              case ty of
                NamedIndividual | rel == Just Types -> do
                  inD <- mapIndivURI cSig iri
                  return (map (mk1VDecl . mkImpl (mkEqDecl 1 inD)) els,
                        uniteL $ cSig : s)
                DataProperty | rel == (Just $ DRRelation ADomain) -> do
                  oEx <- mapDataProp cSig iri 1 2
                  let vars = (mkNName 1, mkNName 2)
                  return (map (mkFEI [tokDecl $ fst vars]
                       [mkVarDecl (snd vars) dataS] oEx) els, uniteL $ cSig : s)
                _ -> failMsg lfb
          ObjectEntity oe -> case rel of
              Nothing -> failMsg lfb
              Just re -> case re of
                  DRRelation r -> do
                    tobjP <- mapObjProp cSig oe 1 2
                    (tdsc, s) <- mapAndUnzipM (\ (_, c) -> mapDescription cSig c
                        $ case r of
                                ADomain -> 1
                                ARange -> 2) cls
                    let vars = case r of
                                ADomain -> (mkNName 1, mkNName 2)
                                ARange -> (mkNName 2, mkNName 1)
                    return (map (mkFEI [tokDecl $ fst vars]
                            [tokDecl $ snd vars] tobjP) tdsc, uniteL $ cSig : s)
                  _ -> failMsg lfb
          ClassEntity ce -> let cel = map snd cls in case rel of
              Nothing -> return ([], cSig)
              Just r -> case r of
                EDRelation _ -> do
                    (decrsS, s) <- mapDescriptionListP cSig 1 $ mkPairs ce cel
                    mkEDPairs (uniteCASLSign cSig s) [1] rel decrsS
                SubClass -> do
                  (domT, s1) <- mapDescription cSig ce 1
                  (codT, s2) <- mapDescriptionList cSig 1 cel
                  return (map (mk1VDecl . mkImpl domT) codT,
                        uniteL [cSig, s1, s2])
                _ -> failMsg lfb
    ObjectBit ol -> let opl = map snd ol in case rel of
      Nothing -> failMsg lfb
      Just r -> case ex of
        Misc _ -> do
            pairs <- mapComObjectPropsList cSig Nothing opl 1 2
            mkEDPairs cSig [1, 2] rel pairs
        ObjectEntity op -> case r of
            EDRelation _ -> do
                pairs <- mapComObjectPropsList cSig (Just op) opl 1 2
                mkEDPairs cSig [1, 2] rel pairs
            SubPropertyOf -> do
                os <- mapM (\ (o1, o2) -> mapSubObjProp cSig o1 o2 3)
                    $ mkPairs op opl
                return (os, cSig)
            InverseOf -> do
                os1 <- mapM (\ o1 -> mapObjProp cSig o1 1 2) opl
                o2 <- mapObjProp cSig op 2 1
                return (map (mkVDecl [1, 2] . mkEqv o2) os1, cSig)
            _ -> failMsg lfb
        _ -> failMsg lfb
    DataBit anl -> let dl = map snd anl in case rel of
      Nothing -> return ([], cSig)
      Just r -> case ex of
        Misc _ -> do
            pairs <- mapComDataPropsList cSig Nothing dl 1 2
            mkEDPairs cSig [1, 2] rel pairs
        SimpleEntity (Entity DataProperty iri) -> case r of
            SubPropertyOf -> do
                os1 <- mapM (\ o1 -> mapDataProp cSig o1 1 2) dl
                o2 <- mapDataProp cSig iri 2 1
                return (map (mkForall [thingDecl 1, dataDecl 2]
                    . mkImpl o2) os1, cSig)
            EDRelation _ -> do
                pairs <- mapComDataPropsList cSig (Just iri) dl 1 2
                mkEDPairs cSig [1, 2] rel pairs
            _ -> return ([], cSig)
        _ -> failMsg lfb
    IndividualSameOrDifferent al -> case rel of
        Nothing -> failMsg lfb
        Just (SDRelation re) -> do
            let SimpleEntity (Entity NamedIndividual iri) = ex
            fs <- mapComIndivList cSig re (Just iri) $ map snd al
            return (fs, cSig)
        _ -> failMsg lfb
    DataPropRange dpr -> case ex of
        SimpleEntity (Entity DataProperty iri) -> do
            oEx <- mapDataProp cSig iri 1 2
            (odes, s) <- mapAndUnzipM (\ (_, c) -> mapDataRange cSig c 2) dpr
            let vars = (mkNName 1, mkNName 2)
            return (map (mkFEI [tokDecl $ fst vars]
                        [tokDataDecl $ snd vars] oEx) odes, uniteL $ cSig : s)
        _ -> failMsg lfb
    IndividualFacts indf -> do
        fl <- mapM (mapFact cSig ex . snd) indf
        return (fl, cSig)
    ObjectCharacteristics ace -> case ex of
        ObjectEntity ope -> do
            cl <- mapM (mapCharact cSig ope . snd) ace
            return (cl, cSig)
        _ -> failMsg ace

-- | Mapping of AnnFrameBit
mapAnnFrameBit :: CASLSign -> Extended -> AnnFrameBit
            -> Result ([CASLFORMULA], CASLSign)
mapAnnFrameBit cSig ex afb =
    let err = fail $ "could not translate " ++ show afb in case afb of
    AnnotationFrameBit _ -> return ([], cSig)
    DataFunctional -> case ex of
        SimpleEntity (Entity _ iri) -> do
            so1 <- mapDataProp cSig iri 1 2
            so2 <- mapDataProp cSig iri 1 3
            return ([mkForall (thingDecl 1 : map dataDecl [2, 3]) $ implConj
                        [so1, so2] $ mkEqVar (dataDecl 2) $ qualData 3], cSig)
        _ -> err
    DatatypeBit dr -> case ex of
        SimpleEntity (Entity Datatype iri) -> do
            (odes, s) <- mapDataRange cSig dr 2
            return ([mkVDataDecl [2] $ mkEqv odes $ mkMember
                    (qualData 2) $ uriToCaslId iri], uniteCASLSign cSig s)
        _ -> err
    ClassDisjointUnion clsl -> case ex of
        SimpleEntity (Entity Class iri) -> do
            (decrs, s1) <- mapDescriptionList cSig 1 clsl
            (decrsS, s2) <- mapDescriptionListP cSig 1 $ comPairs clsl clsl
            let decrsP = map (\ (x, y) -> conjunct [x, y]) decrsS
            mcls <- mapClassURI cSig iri $ mkNName 1
            return ([mk1VDecl $ mkEqv mcls $ conjunct
                    [disjunct decrs, mkNC decrsP]], uniteL [cSig, s1, s2])
        _ -> err
    ClassHasKey opl dpl -> do
        let ClassEntity ce = ex
            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 cSig o 1 n) $ zip uptoOP opl
        nol <- mapM (\ (n, o) -> mapObjProp cSig o tl n) $ zip uptoOP opl
        dl <- mapM (\ (n, d) -> mapDataProp cSig d 1 n) $ zip uptoDP dpl
        ndl <- mapM (\ (n, d) -> mapDataProp cSig d tl n) $ zip uptoDP dpl
        (keys, s) <-
            mapKey cSig ce (ol ++ dl) (nol ++ ndl) tl (uptoOP ++ uptoDP) lo
        return ([keys], uniteCASLSign cSig s)
    ObjectSubPropertyChain oplst -> do
        os <- mapM (\ cd -> mapSubObjPropChain cSig oplst cd 3) oplst
        return (os, cSig)

keyDecl :: Int -> [Int] -> [VAR_DECL]
keyDecl h il = map thingDecl (take h il) ++ map dataDecl (drop h il)

mapKey :: CASLSign -> ClassExpression -> [FORMULA ()] -> [FORMULA ()]
    -> Int -> [Int] -> Int -> Result (FORMULA (), CASLSign)
mapKey cSig ce pl npl p i h = do
    (nce, s) <- mapDescription cSig ce 1
    (c3, _) <- mapDescription cSig 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 :: CASLSign -> Axiom -> Result ([CASLFORMULA], CASLSign)
mapAxioms cSig (PlainAxiom ex fb) = case fb of
    ListFrameBit rel lfb -> mapListFrameBit cSig ex rel lfb
    AnnFrameBit _ afb -> mapAnnFrameBit cSig ex afb
