{-# 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 Int -> OWL22CASL -> ShowS
[OWL22CASL] -> ShowS
OWL22CASL -> String
(Int -> OWL22CASL -> ShowS)
-> (OWL22CASL -> String)
-> ([OWL22CASL] -> ShowS)
-> Show OWL22CASL
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [OWL22CASL] -> ShowS
$cshowList :: [OWL22CASL] -> ShowS
show :: OWL22CASL -> String
$cshow :: OWL22CASL -> String
showsPrec :: Int -> OWL22CASL -> ShowS
$cshowsPrec :: Int -> OWL22CASL -> ShowS
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
sourceLogic OWL22CASL = OWL2
OWL2
      sourceSublogic :: OWL22CASL -> ProfSub
sourceSublogic OWL22CASL = ProfSub
topS
      targetLogic :: OWL22CASL -> CASL
targetLogic OWL22CASL = CASL
CASL
      mapSublogic :: OWL22CASL -> ProfSub -> Maybe CASL_Sublogics
mapSublogic OWL22CASL _ = CASL_Sublogics -> Maybe CASL_Sublogics
forall a. a -> Maybe a
Just (CASL_Sublogics -> Maybe CASL_Sublogics)
-> CASL_Sublogics -> Maybe CASL_Sublogics
forall a b. (a -> b) -> a -> b
$ CASL_Sublogics
forall a. Lattice a => CASL_SL a
cFol
        { cons_features :: SortGenerationFeatures
cons_features = SortGenerationFeatures
emptyMapConsFeature }
      map_theory :: OWL22CASL
-> (Sign, [Named Axiom]) -> Result (CASLSign, [Named CASLFORMULA])
map_theory OWL22CASL = (Sign, [Named Axiom]) -> Result (CASLSign, [Named CASLFORMULA])
mapTheory
      map_morphism :: OWL22CASL -> OWLMorphism -> Result CASLMor
map_morphism OWL22CASL = OWLMorphism -> Result CASLMor
mapMorphism
      map_symbol :: OWL22CASL -> Sign -> Entity -> Set Symbol
map_symbol OWL22CASL _ = Entity -> Set Symbol
mapSymbol
      isInclusionComorphism :: OWL22CASL -> Bool
isInclusionComorphism OWL22CASL = Bool
True
      has_model_expansion :: OWL22CASL -> Bool
has_model_expansion OWL22CASL = Bool
True

-- s = emptySign ()

objectPropPred :: PredType
objectPropPred :: PredType
objectPropPred = [SORT] -> PredType
PredType [SORT
thing, SORT
thing]

dataPropPred :: PredType
dataPropPred :: PredType
dataPropPred = [SORT] -> PredType
PredType [SORT
thing, SORT
dataS]

indiConst :: OpType
indiConst :: OpType
indiConst = OpKind -> [SORT] -> SORT -> OpType
OpType OpKind
Total [] SORT
thing


uriToIdM :: IRI -> Result Id
uriToIdM :: IRI -> Result SORT
uriToIdM = SORT -> Result SORT
forall (m :: * -> *) a. Monad m => a -> m a
return (SORT -> Result SORT) -> (IRI -> SORT) -> IRI -> Result SORT
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IRI -> SORT
uriToCaslId

tokDecl :: Token -> VAR_DECL
tokDecl :: Token -> VAR_DECL
tokDecl = (Token -> SORT -> VAR_DECL) -> SORT -> Token -> VAR_DECL
forall a b c. (a -> b -> c) -> b -> a -> c
flip Token -> SORT -> VAR_DECL
mkVarDecl SORT
thing

tokDataDecl :: Token -> VAR_DECL
tokDataDecl :: Token -> VAR_DECL
tokDataDecl = (Token -> SORT -> VAR_DECL) -> SORT -> Token -> VAR_DECL
forall a b c. (a -> b -> c) -> b -> a -> c
flip Token -> SORT -> VAR_DECL
mkVarDecl SORT
dataS

nameDecl :: Int -> SORT -> VAR_DECL
nameDecl :: Int -> SORT -> VAR_DECL
nameDecl = Token -> SORT -> VAR_DECL
mkVarDecl (Token -> SORT -> VAR_DECL)
-> (Int -> Token) -> Int -> SORT -> VAR_DECL
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Token
mkNName

thingDecl :: Int -> VAR_DECL
thingDecl :: Int -> VAR_DECL
thingDecl = (Int -> SORT -> VAR_DECL) -> SORT -> Int -> VAR_DECL
forall a b c. (a -> b -> c) -> b -> a -> c
flip Int -> SORT -> VAR_DECL
nameDecl SORT
thing

dataDecl :: Int -> VAR_DECL
dataDecl :: Int -> VAR_DECL
dataDecl = (Int -> SORT -> VAR_DECL) -> SORT -> Int -> VAR_DECL
forall a b c. (a -> b -> c) -> b -> a -> c
flip Int -> SORT -> VAR_DECL
nameDecl SORT
dataS

qualThing :: Int -> TERM f
qualThing :: Int -> TERM f
qualThing = VAR_DECL -> TERM f
forall f. VAR_DECL -> TERM f
toQualVar (VAR_DECL -> TERM f) -> (Int -> VAR_DECL) -> Int -> TERM f
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> VAR_DECL
thingDecl

qualData :: Int -> TERM f
qualData :: Int -> TERM f
qualData = VAR_DECL -> TERM f
forall f. VAR_DECL -> TERM f
toQualVar (VAR_DECL -> TERM f) -> (Int -> VAR_DECL) -> Int -> TERM f
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> VAR_DECL
dataDecl

implConj :: [FORMULA f] -> FORMULA f -> FORMULA f
implConj :: [FORMULA f] -> FORMULA f -> FORMULA f
implConj = FORMULA f -> FORMULA f -> FORMULA f
forall f. FORMULA f -> FORMULA f -> FORMULA f
mkImpl (FORMULA f -> FORMULA f -> FORMULA f)
-> ([FORMULA f] -> FORMULA f)
-> [FORMULA f]
-> FORMULA f
-> FORMULA f
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [FORMULA f] -> FORMULA f
forall f. [FORMULA f] -> FORMULA f
conjunct

mkNC :: [FORMULA f] -> FORMULA f
mkNC :: [FORMULA f] -> FORMULA f
mkNC = FORMULA f -> FORMULA f
forall f. FORMULA f -> FORMULA f
mkNeg (FORMULA f -> FORMULA f)
-> ([FORMULA f] -> FORMULA f) -> [FORMULA f] -> FORMULA f
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [FORMULA f] -> FORMULA f
forall f. [FORMULA f] -> FORMULA f
conjunct

mkEqVar :: VAR_DECL -> TERM f -> FORMULA f
mkEqVar :: VAR_DECL -> TERM f -> FORMULA f
mkEqVar = TERM f -> TERM f -> FORMULA f
forall f. TERM f -> TERM f -> FORMULA f
mkStEq (TERM f -> TERM f -> FORMULA f)
-> (VAR_DECL -> TERM f) -> VAR_DECL -> TERM f -> FORMULA f
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VAR_DECL -> TERM f
forall f. VAR_DECL -> TERM f
toQualVar

mkFEI :: [VAR_DECL] -> [VAR_DECL] -> FORMULA f -> FORMULA f -> FORMULA f
mkFEI :: [VAR_DECL] -> [VAR_DECL] -> FORMULA f -> FORMULA f -> FORMULA f
mkFEI l1 :: [VAR_DECL]
l1 l2 :: [VAR_DECL]
l2 f :: FORMULA f
f = [VAR_DECL] -> FORMULA f -> FORMULA f
forall f. [VAR_DECL] -> FORMULA f -> FORMULA f
mkForall [VAR_DECL]
l1 (FORMULA f -> FORMULA f)
-> (FORMULA f -> FORMULA f) -> FORMULA f -> FORMULA f
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [VAR_DECL] -> FORMULA f -> FORMULA f
forall f. [VAR_DECL] -> FORMULA f -> FORMULA f
mkExist [VAR_DECL]
l2 (FORMULA f -> FORMULA f)
-> (FORMULA f -> FORMULA f) -> FORMULA f -> FORMULA f
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FORMULA f -> FORMULA f -> FORMULA f
forall f. FORMULA f -> FORMULA f -> FORMULA f
mkImpl FORMULA f
f

mkFIE :: [Int] -> [FORMULA f] -> Int -> Int -> FORMULA f
mkFIE :: [Int] -> [FORMULA f] -> Int -> Int -> FORMULA f
mkFIE l1 :: [Int]
l1 l2 :: [FORMULA f]
l2 x :: Int
x y :: Int
y = [Int] -> FORMULA f -> FORMULA f
forall f. [Int] -> FORMULA f -> FORMULA f
mkVDecl [Int]
l1 (FORMULA f -> FORMULA f) -> FORMULA f -> FORMULA f
forall a b. (a -> b) -> a -> b
$ [FORMULA f] -> FORMULA f -> FORMULA f
forall f. [FORMULA f] -> FORMULA f -> FORMULA f
implConj [FORMULA f]
l2 (FORMULA f -> FORMULA f) -> FORMULA f -> FORMULA f
forall a b. (a -> b) -> a -> b
$ VAR_DECL -> TERM f -> FORMULA f
forall f. VAR_DECL -> TERM f -> FORMULA f
mkEqVar (Int -> VAR_DECL
thingDecl Int
x) (TERM f -> FORMULA f) -> TERM f -> FORMULA f
forall a b. (a -> b) -> a -> b
$ Int -> TERM f
forall f. Int -> TERM f
qualThing Int
y

mkFI :: [VAR_DECL] -> [VAR_DECL] -> FORMULA f -> FORMULA f -> FORMULA f
mkFI :: [VAR_DECL] -> [VAR_DECL] -> FORMULA f -> FORMULA f -> FORMULA f
mkFI l1 :: [VAR_DECL]
l1 l2 :: [VAR_DECL]
l2 f1 :: FORMULA f
f1 = ([VAR_DECL] -> FORMULA f -> FORMULA f
forall f. [VAR_DECL] -> FORMULA f -> FORMULA f
mkForall [VAR_DECL]
l1) (FORMULA f -> FORMULA f)
-> (FORMULA f -> FORMULA f) -> FORMULA f -> FORMULA f
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (FORMULA f -> FORMULA f -> FORMULA f
forall f. FORMULA f -> FORMULA f -> FORMULA f
mkImpl ([VAR_DECL] -> FORMULA f -> FORMULA f
forall f. [VAR_DECL] -> FORMULA f -> FORMULA f
mkExist [VAR_DECL]
l2 FORMULA f
f1))

mkRI :: [Int] -> Int -> FORMULA f -> FORMULA f
mkRI :: [Int] -> Int -> FORMULA f -> FORMULA f
mkRI l :: [Int]
l x :: Int
x so :: FORMULA f
so = [Int] -> FORMULA f -> FORMULA f
forall f. [Int] -> FORMULA f -> FORMULA f
mkVDecl [Int]
l (FORMULA f -> FORMULA f) -> FORMULA f -> FORMULA f
forall a b. (a -> b) -> a -> b
$ FORMULA f -> FORMULA f -> FORMULA f
forall f. FORMULA f -> FORMULA f -> FORMULA f
mkImpl (TERM f -> SORT -> FORMULA f
forall f. TERM f -> SORT -> FORMULA f
mkMember (Int -> TERM f
forall f. Int -> TERM f
qualThing Int
x) SORT
thing) FORMULA f
so

mkThingVar :: VAR -> TERM f
mkThingVar :: Token -> TERM f
mkThingVar v :: Token
v = Token -> SORT -> Range -> TERM f
forall f. Token -> SORT -> Range -> TERM f
Qual_var Token
v SORT
thing Range
nullRange

mkEqDecl :: Int -> TERM f -> FORMULA f
mkEqDecl :: Int -> TERM f -> FORMULA f
mkEqDecl i :: Int
i = VAR_DECL -> TERM f -> FORMULA f
forall f. VAR_DECL -> TERM f -> FORMULA f
mkEqVar (Int -> VAR_DECL
thingDecl Int
i)

mkVDecl :: [Int] -> FORMULA f -> FORMULA f
mkVDecl :: [Int] -> FORMULA f -> FORMULA f
mkVDecl = [VAR_DECL] -> FORMULA f -> FORMULA f
forall f. [VAR_DECL] -> FORMULA f -> FORMULA f
mkForall ([VAR_DECL] -> FORMULA f -> FORMULA f)
-> ([Int] -> [VAR_DECL]) -> [Int] -> FORMULA f -> FORMULA f
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int -> VAR_DECL) -> [Int] -> [VAR_DECL]
forall a b. (a -> b) -> [a] -> [b]
map Int -> VAR_DECL
thingDecl

mkVDataDecl :: [Int] -> FORMULA f -> FORMULA f
mkVDataDecl :: [Int] -> FORMULA f -> FORMULA f
mkVDataDecl = [VAR_DECL] -> FORMULA f -> FORMULA f
forall f. [VAR_DECL] -> FORMULA f -> FORMULA f
mkForall ([VAR_DECL] -> FORMULA f -> FORMULA f)
-> ([Int] -> [VAR_DECL]) -> [Int] -> FORMULA f -> FORMULA f
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int -> VAR_DECL) -> [Int] -> [VAR_DECL]
forall a b. (a -> b) -> [a] -> [b]
map Int -> VAR_DECL
dataDecl

mk1VDecl :: FORMULA f -> FORMULA f
mk1VDecl :: FORMULA f -> FORMULA f
mk1VDecl = [Int] -> FORMULA f -> FORMULA f
forall f. [Int] -> FORMULA f -> FORMULA f
mkVDecl [1]

mkPred :: PredType -> [TERM f] -> PRED_NAME -> FORMULA f
mkPred :: PredType -> [TERM f] -> SORT -> FORMULA f
mkPred c :: PredType
c tl :: [TERM f]
tl u :: SORT
u = PRED_SYMB -> [TERM f] -> FORMULA f
forall f. PRED_SYMB -> [TERM f] -> FORMULA f
mkPredication (SORT -> PRED_TYPE -> PRED_SYMB
mkQualPred SORT
u (PRED_TYPE -> PRED_SYMB) -> PRED_TYPE -> PRED_SYMB
forall a b. (a -> b) -> a -> b
$ PredType -> PRED_TYPE
toPRED_TYPE PredType
c) [TERM f]
tl

mkMember :: TERM f -> SORT -> FORMULA f
mkMember :: TERM f -> SORT -> FORMULA f
mkMember t :: TERM f
t s :: SORT
s = TERM f -> SORT -> Range -> FORMULA f
forall f. TERM f -> SORT -> Range -> FORMULA f
Membership TERM f
t SORT
s Range
nullRange

-- | Get all distinct pairs for commutative operations
comPairs :: [t] -> [t1] -> [(t, t1)]
comPairs :: [t] -> [t1] -> [(t, t1)]
comPairs [] [] = []
comPairs _ [] = []
comPairs [] _ = []
comPairs (a :: t
a : as :: [t]
as) (_ : bs :: [t1]
bs) = t -> [t1] -> [(t, t1)]
forall t s. t -> [s] -> [(t, s)]
mkPairs t
a [t1]
bs [(t, t1)] -> [(t, t1)] -> [(t, t1)]
forall a. [a] -> [a] -> [a]
++ [t] -> [t1] -> [(t, t1)]
forall t t1. [t] -> [t1] -> [(t, t1)]
comPairs [t]
as [t1]
bs

mkPairs :: t -> [s] -> [(t, s)]
mkPairs :: t -> [s] -> [(t, s)]
mkPairs a :: t
a = (s -> (t, s)) -> [s] -> [(t, s)]
forall a b. (a -> b) -> [a] -> [b]
map (\ b :: s
b -> (t
a, s
b))

data VarOrIndi = OVar Int | OIndi IRI
    deriving (Int -> VarOrIndi -> ShowS
[VarOrIndi] -> ShowS
VarOrIndi -> String
(Int -> VarOrIndi -> ShowS)
-> (VarOrIndi -> String)
-> ([VarOrIndi] -> ShowS)
-> Show VarOrIndi
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [VarOrIndi] -> ShowS
$cshowList :: [VarOrIndi] -> ShowS
show :: VarOrIndi -> String
$cshow :: VarOrIndi -> String
showsPrec :: Int -> VarOrIndi -> ShowS
$cshowsPrec :: Int -> VarOrIndi -> ShowS
Show, VarOrIndi -> VarOrIndi -> Bool
(VarOrIndi -> VarOrIndi -> Bool)
-> (VarOrIndi -> VarOrIndi -> Bool) -> Eq VarOrIndi
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: VarOrIndi -> VarOrIndi -> Bool
$c/= :: VarOrIndi -> VarOrIndi -> Bool
== :: VarOrIndi -> VarOrIndi -> Bool
$c== :: VarOrIndi -> VarOrIndi -> Bool
Eq, Eq VarOrIndi
Eq VarOrIndi =>
(VarOrIndi -> VarOrIndi -> Ordering)
-> (VarOrIndi -> VarOrIndi -> Bool)
-> (VarOrIndi -> VarOrIndi -> Bool)
-> (VarOrIndi -> VarOrIndi -> Bool)
-> (VarOrIndi -> VarOrIndi -> Bool)
-> (VarOrIndi -> VarOrIndi -> VarOrIndi)
-> (VarOrIndi -> VarOrIndi -> VarOrIndi)
-> Ord VarOrIndi
VarOrIndi -> VarOrIndi -> Bool
VarOrIndi -> VarOrIndi -> Ordering
VarOrIndi -> VarOrIndi -> VarOrIndi
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: VarOrIndi -> VarOrIndi -> VarOrIndi
$cmin :: VarOrIndi -> VarOrIndi -> VarOrIndi
max :: VarOrIndi -> VarOrIndi -> VarOrIndi
$cmax :: VarOrIndi -> VarOrIndi -> VarOrIndi
>= :: VarOrIndi -> VarOrIndi -> Bool
$c>= :: VarOrIndi -> VarOrIndi -> Bool
> :: VarOrIndi -> VarOrIndi -> Bool
$c> :: VarOrIndi -> VarOrIndi -> Bool
<= :: VarOrIndi -> VarOrIndi -> Bool
$c<= :: VarOrIndi -> VarOrIndi -> Bool
< :: VarOrIndi -> VarOrIndi -> Bool
$c< :: VarOrIndi -> VarOrIndi -> Bool
compare :: VarOrIndi -> VarOrIndi -> Ordering
$ccompare :: VarOrIndi -> VarOrIndi -> Ordering
$cp1Ord :: Eq VarOrIndi
Ord)

-- | Mapping of OWL morphisms to CASL morphisms
mapMorphism :: OWLMorphism -> Result CASLMor
mapMorphism :: OWLMorphism -> Result CASLMor
mapMorphism oMor :: OWLMorphism
oMor = do
      CASLSign
cdm <- Sign -> Result CASLSign
mapSign (Sign -> Result CASLSign) -> Sign -> Result CASLSign
forall a b. (a -> b) -> a -> b
$ OWLMorphism -> Sign
osource OWLMorphism
oMor
      CASLSign
ccd <- Sign -> Result CASLSign
mapSign (Sign -> Result CASLSign) -> Sign -> Result CASLSign
forall a b. (a -> b) -> a -> b
$ OWLMorphism -> Sign
otarget OWLMorphism
oMor
      let emap :: MorphMap
emap = OWLMorphism -> MorphMap
mmaps OWLMorphism
oMor
          preds :: Map (SORT, PredType) SORT
preds = (Entity
 -> IRI -> Map (SORT, PredType) SORT -> Map (SORT, PredType) SORT)
-> Map (SORT, PredType) SORT
-> MorphMap
-> Map (SORT, PredType) SORT
forall k a b. (k -> a -> b -> b) -> b -> Map k a -> b
Map.foldrWithKey (\ (Entity _ ty :: EntityType
ty u1 :: IRI
u1) u2 :: IRI
u2 -> let
              i1 :: SORT
i1 = IRI -> SORT
uriToCaslId IRI
u1
              i2 :: SORT
i2 = IRI -> SORT
uriToCaslId IRI
u2
              in case EntityType
ty of
                Class -> (SORT, PredType)
-> SORT -> Map (SORT, PredType) SORT -> Map (SORT, PredType) SORT
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (SORT
i1, PredType
conceptPred) SORT
i2
                ObjectProperty -> (SORT, PredType)
-> SORT -> Map (SORT, PredType) SORT -> Map (SORT, PredType) SORT
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (SORT
i1, PredType
objectPropPred) SORT
i2
                DataProperty -> (SORT, PredType)
-> SORT -> Map (SORT, PredType) SORT -> Map (SORT, PredType) SORT
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (SORT
i1, PredType
dataPropPred) SORT
i2
                _ -> Map (SORT, PredType) SORT -> Map (SORT, PredType) SORT
forall a. a -> a
id) Map (SORT, PredType) SORT
forall k a. Map k a
Map.empty MorphMap
emap
          ops :: Map (SORT, OpType) (SORT, OpKind)
ops = (Entity
 -> IRI
 -> Map (SORT, OpType) (SORT, OpKind)
 -> Map (SORT, OpType) (SORT, OpKind))
-> Map (SORT, OpType) (SORT, OpKind)
-> MorphMap
-> Map (SORT, OpType) (SORT, OpKind)
forall k a b. (k -> a -> b -> b) -> b -> Map k a -> b
Map.foldrWithKey (\ (Entity _ ty :: EntityType
ty u1 :: IRI
u1) u2 :: IRI
u2 -> case EntityType
ty of
                NamedIndividual -> (SORT, OpType)
-> (SORT, OpKind)
-> Map (SORT, OpType) (SORT, OpKind)
-> Map (SORT, OpType) (SORT, OpKind)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (IRI -> SORT
uriToCaslId IRI
u1, OpType
indiConst)
                  (IRI -> SORT
uriToCaslId IRI
u2, OpKind
Total)
                _ -> Map (SORT, OpType) (SORT, OpKind)
-> Map (SORT, OpType) (SORT, OpKind)
forall a. a -> a
id) Map (SORT, OpType) (SORT, OpKind)
forall k a. Map k a
Map.empty MorphMap
emap
      CASLMor -> Result CASLMor
forall (m :: * -> *) a. Monad m => a -> m a
return (() -> CASLSign -> CASLSign -> CASLMor
forall m f e. m -> Sign f e -> Sign f e -> Morphism f e m
embedMorphism () CASLSign
cdm CASLSign
ccd)
                 { op_map :: Map (SORT, OpType) (SORT, OpKind)
op_map = Map (SORT, OpType) (SORT, OpKind)
ops
                 , pred_map :: Map (SORT, PredType) SORT
pred_map = Map (SORT, PredType) SORT
preds }

mapSymbol :: Entity -> Set.Set Symbol
mapSymbol :: Entity -> Set Symbol
mapSymbol (Entity _ ty :: EntityType
ty iRi :: IRI
iRi) = let
  syN :: SymbType -> Set Symbol
syN = Symbol -> Set Symbol
forall a. a -> Set a
Set.singleton (Symbol -> Set Symbol)
-> (SymbType -> Symbol) -> SymbType -> Set Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SORT -> SymbType -> Symbol
Symbol (IRI -> SORT
uriToCaslId IRI
iRi)
  in case EntityType
ty of
    Class -> SymbType -> Set Symbol
syN (SymbType -> Set Symbol) -> SymbType -> Set Symbol
forall a b. (a -> b) -> a -> b
$ PredType -> SymbType
PredAsItemType PredType
conceptPred
    ObjectProperty -> SymbType -> Set Symbol
syN (SymbType -> Set Symbol) -> SymbType -> Set Symbol
forall a b. (a -> b) -> a -> b
$ PredType -> SymbType
PredAsItemType PredType
objectPropPred
    DataProperty -> SymbType -> Set Symbol
syN (SymbType -> Set Symbol) -> SymbType -> Set Symbol
forall a b. (a -> b) -> a -> b
$ PredType -> SymbType
PredAsItemType PredType
dataPropPred
    NamedIndividual -> SymbType -> Set Symbol
syN (SymbType -> Set Symbol) -> SymbType -> Set Symbol
forall a b. (a -> b) -> a -> b
$ OpType -> SymbType
OpAsItemType OpType
indiConst
    AnnotationProperty -> Set Symbol
forall a. Set a
Set.empty
    Datatype -> Set Symbol
forall a. Set a
Set.empty

mapSign :: OS.Sign -> Result CASLSign
mapSign :: Sign -> Result CASLSign
mapSign sig :: Sign
sig =
      let conc :: Set IRI
conc = Sign -> Set IRI
OS.concepts Sign
sig
          cvrt :: Set IRI -> [SORT]
cvrt = (IRI -> SORT) -> [IRI] -> [SORT]
forall a b. (a -> b) -> [a] -> [b]
map IRI -> SORT
uriToCaslId ([IRI] -> [SORT]) -> (Set IRI -> [IRI]) -> Set IRI -> [SORT]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set IRI -> [IRI]
forall a. Set a -> [a]
Set.toList
          tMp :: b -> [a] -> MapSet a b
tMp k :: b
k = [(a, [b])] -> MapSet a b
forall a b. (Ord a, Ord b) => [(a, [b])] -> MapSet a b
MapSet.fromList ([(a, [b])] -> MapSet a b)
-> ([a] -> [(a, [b])]) -> [a] -> MapSet a b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> (a, [b])) -> [a] -> [(a, [b])]
forall a b. (a -> b) -> [a] -> [b]
map (\ u :: a
u -> (a
u, [b
k]))
          cPreds :: [SORT]
cPreds = SORT
thing SORT -> [SORT] -> [SORT]
forall a. a -> [a] -> [a]
: SORT
nothing SORT -> [SORT] -> [SORT]
forall a. a -> [a] -> [a]
: Set IRI -> [SORT]
cvrt Set IRI
conc
          oPreds :: [SORT]
oPreds = Set IRI -> [SORT]
cvrt (Set IRI -> [SORT]) -> Set IRI -> [SORT]
forall a b. (a -> b) -> a -> b
$ Sign -> Set IRI
OS.objectProperties Sign
sig
          dPreds :: [SORT]
dPreds = Set IRI -> [SORT]
cvrt (Set IRI -> [SORT]) -> Set IRI -> [SORT]
forall a b. (a -> b) -> a -> b
$ Sign -> Set IRI
OS.dataProperties Sign
sig
          aPreds :: MapSet SORT PredType
aPreds = (MapSet SORT PredType
 -> MapSet SORT PredType -> MapSet SORT PredType)
-> MapSet SORT PredType
-> [MapSet SORT PredType]
-> MapSet SORT PredType
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr MapSet SORT PredType
-> MapSet SORT PredType -> MapSet SORT PredType
forall a b.
(Ord a, Ord b) =>
MapSet a b -> MapSet a b -> MapSet a b
MapSet.union MapSet SORT PredType
forall a b. MapSet a b
MapSet.empty
            [ PredType -> [SORT] -> MapSet SORT PredType
forall a b. (Ord a, Ord b) => b -> [a] -> MapSet a b
tMp PredType
conceptPred [SORT]
cPreds
            , PredType -> [SORT] -> MapSet SORT PredType
forall a b. (Ord a, Ord b) => b -> [a] -> MapSet a b
tMp PredType
objectPropPred [SORT]
oPreds
            , PredType -> [SORT] -> MapSet SORT PredType
forall a b. (Ord a, Ord b) => b -> [a] -> MapSet a b
tMp PredType
dataPropPred [SORT]
dPreds ]
     in CASLSign -> Result CASLSign
forall (m :: * -> *) a. Monad m => a -> m a
return (CASLSign -> Result CASLSign) -> CASLSign -> Result CASLSign
forall a b. (a -> b) -> a -> b
$  CASLSign -> CASLSign -> CASLSign
uniteCASLSign CASLSign
predefSign2
         (() -> CASLSign
forall e f. e -> Sign f e
emptySign ())
             { predMap :: MapSet SORT PredType
predMap = MapSet SORT PredType
aPreds
             , opMap :: OpMap
opMap = OpType -> [SORT] -> OpMap
forall a b. (Ord a, Ord b) => b -> [a] -> MapSet a b
tMp OpType
indiConst ([SORT] -> OpMap) -> (Set IRI -> [SORT]) -> Set IRI -> OpMap
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set IRI -> [SORT]
cvrt (Set IRI -> OpMap) -> Set IRI -> OpMap
forall a b. (a -> b) -> a -> b
$ Sign -> Set IRI
OS.individuals Sign
sig
             }

loadDataInformation :: ProfSub -> CASLSign
loadDataInformation :: ProfSub -> CASLSign
loadDataInformation sl :: ProfSub
sl = let
  dts :: Set SORT
dts = (IRI -> SORT) -> Set IRI -> Set SORT
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map IRI -> SORT
uriToCaslId (Set IRI -> Set SORT) -> Set IRI -> Set SORT
forall a b. (a -> b) -> a -> b
$ OWLSub -> Set IRI
SL.datatype (OWLSub -> Set IRI) -> OWLSub -> Set IRI
forall a b. (a -> b) -> a -> b
$ ProfSub -> OWLSub
sublogic ProfSub
sl
  eSig :: SORT -> Sign f ()
eSig x :: SORT
x = (() -> Sign f ()
forall e f. e -> Sign f e
emptySign ()) { sortRel :: Rel SORT
sortRel =
       [(SORT, SORT)] -> Rel SORT
forall a. Ord a => [(a, a)] -> Rel a
Rel.fromList  [(SORT
x, SORT
dataS)]}
  sigs :: [CASLSign]
sigs = Set CASLSign -> [CASLSign]
forall a. Set a -> [a]
Set.toList (Set CASLSign -> [CASLSign]) -> Set CASLSign -> [CASLSign]
forall a b. (a -> b) -> a -> b
$
         (SORT -> CASLSign) -> Set SORT -> Set CASLSign
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (\x :: SORT
x -> CASLSign -> SORT -> Map SORT CASLSign -> CASLSign
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault (SORT -> CASLSign
forall f. SORT -> Sign f ()
eSig SORT
x) SORT
x Map SORT CASLSign
datatypeSigns) Set SORT
dts
 in  (CASLSign -> CASLSign -> CASLSign)
-> CASLSign -> [CASLSign] -> CASLSign
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl CASLSign -> CASLSign -> CASLSign
uniteCASLSign (() -> CASLSign
forall e f. e -> Sign f e
emptySign ()) [CASLSign]
sigs

mapTheory :: (OS.Sign, [Named Axiom]) -> Result (CASLSign, [Named CASLFORMULA])
mapTheory :: (Sign, [Named Axiom]) -> Result (CASLSign, [Named CASLFORMULA])
mapTheory (owlSig :: Sign
owlSig, owlSens :: [Named Axiom]
owlSens) = let
  sl :: ProfSub
sl = OWL2 -> (Sign, [Axiom]) -> ProfSub
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> (sign, [sentence]) -> sublogics
sublogicOfTheo OWL2
OWL2 (Sign
owlSig, (Named Axiom -> Axiom) -> [Named Axiom] -> [Axiom]
forall a b. (a -> b) -> [a] -> [b]
map Named Axiom -> Axiom
forall s a. SenAttr s a -> s
sentence [Named Axiom]
owlSens)
 in do
    CASLSign
cSig <- Sign -> Result CASLSign
mapSign Sign
owlSig
    let pSig :: CASLSign
pSig = ProfSub -> CASLSign
loadDataInformation ProfSub
sl
        {- dTypes = (emptySign ()) {sortRel = Rel.transClosure . Rel.fromSet
                    . Set.map (\ d -> (uriToCaslId d, dataS))
                    . Set.union predefIRIs $ OS.datatypes owlSig} -}
    (cSens :: [Named CASLFORMULA]
cSens, nSigs :: [CASLSign]
nSigs) <- (([Named CASLFORMULA], [CASLSign])
 -> Named Axiom -> Result ([Named CASLFORMULA], [CASLSign]))
-> ([Named CASLFORMULA], [CASLSign])
-> [Named Axiom]
-> Result ([Named CASLFORMULA], [CASLSign])
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (\ (x :: [Named CASLFORMULA]
x, y :: [CASLSign]
y) z :: Named Axiom
z -> do
            (sen :: [Named CASLFORMULA]
sen, y' :: [CASLSign]
y') <- Named Axiom -> Result ([Named CASLFORMULA], [CASLSign])
mapSentence Named Axiom
z
            ([Named CASLFORMULA], [CASLSign])
-> Result ([Named CASLFORMULA], [CASLSign])
forall (m :: * -> *) a. Monad m => a -> m a
return ([Named CASLFORMULA]
sen [Named CASLFORMULA] -> [Named CASLFORMULA] -> [Named CASLFORMULA]
forall a. [a] -> [a] -> [a]
++ [Named CASLFORMULA]
x, [CASLSign]
y [CASLSign] -> [CASLSign] -> [CASLSign]
forall a. [a] -> [a] -> [a]
++ [CASLSign]
y')) -- uniteCASLSign sig y)) 
                     ([], []) [Named Axiom]
owlSens
    (CASLSign, [Named CASLFORMULA])
-> Result (CASLSign, [Named CASLFORMULA])
forall (m :: * -> *) a. Monad m => a -> m a
return ((CASLSign -> CASLSign -> CASLSign) -> [CASLSign] -> CASLSign
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldl1 CASLSign -> CASLSign -> CASLSign
uniteCASLSign ([CASLSign] -> CASLSign) -> [CASLSign] -> CASLSign
forall a b. (a -> b) -> a -> b
$ [CASLSign
cSig,CASLSign
pSig] [CASLSign] -> [CASLSign] -> [CASLSign]
forall a. [a] -> [a] -> [a]
++ [CASLSign]
nSigs,  -- , dTypes],
            [Named CASLFORMULA]
predefinedAxioms [Named CASLFORMULA] -> [Named CASLFORMULA] -> [Named CASLFORMULA]
forall a. [a] -> [a] -> [a]
++ ([Named CASLFORMULA] -> [Named CASLFORMULA]
forall a. [a] -> [a]
reverse [Named CASLFORMULA]
cSens))

-- | mapping of OWL to CASL_DL formulae
mapSentence :: Named Axiom -> Result ([Named CASLFORMULA], [CASLSign])
mapSentence :: Named Axiom -> Result ([Named CASLFORMULA], [CASLSign])
mapSentence inSen :: Named Axiom
inSen = do
    (outAx :: [CASLFORMULA]
outAx, outSigs :: [CASLSign]
outSigs) <- Axiom -> Result ([CASLFORMULA], [CASLSign])
mapAxioms (Axiom -> Result ([CASLFORMULA], [CASLSign]))
-> Axiom -> Result ([CASLFORMULA], [CASLSign])
forall a b. (a -> b) -> a -> b
$ Named Axiom -> Axiom
forall s a. SenAttr s a -> s
sentence Named Axiom
inSen
    ([Named CASLFORMULA], [CASLSign])
-> Result ([Named CASLFORMULA], [CASLSign])
forall (m :: * -> *) a. Monad m => a -> m a
return ((CASLFORMULA -> Named CASLFORMULA)
-> [CASLFORMULA] -> [Named CASLFORMULA]
forall a b. (a -> b) -> [a] -> [b]
map (((Axiom -> CASLFORMULA) -> Named Axiom -> Named CASLFORMULA)
-> Named Axiom -> (Axiom -> CASLFORMULA) -> Named CASLFORMULA
forall a b c. (a -> b -> c) -> b -> a -> c
flip (Axiom -> CASLFORMULA) -> Named Axiom -> Named CASLFORMULA
forall s t a. (s -> t) -> SenAttr s a -> SenAttr t a
mapNamed Named Axiom
inSen ((Axiom -> CASLFORMULA) -> Named CASLFORMULA)
-> (CASLFORMULA -> Axiom -> CASLFORMULA)
-> CASLFORMULA
-> Named CASLFORMULA
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CASLFORMULA -> Axiom -> CASLFORMULA
forall a b. a -> b -> a
const) [CASLFORMULA]
outAx, [CASLSign]
outSigs)

mapVar :: VarOrIndi -> Result (TERM ())
mapVar :: VarOrIndi -> Result (TERM ())
mapVar v :: VarOrIndi
v = case VarOrIndi
v of
    OVar n :: Int
n -> TERM () -> Result (TERM ())
forall (m :: * -> *) a. Monad m => a -> m a
return (TERM () -> Result (TERM ())) -> TERM () -> Result (TERM ())
forall a b. (a -> b) -> a -> b
$ Int -> TERM ()
forall f. Int -> TERM f
qualThing Int
n
    OIndi i :: IRI
i -> IRI -> Result (TERM ())
mapIndivURI IRI
i

-- | Mapping of Class URIs
mapClassURI :: Class -> Token -> Result CASLFORMULA
mapClassURI :: IRI -> Token -> Result CASLFORMULA
mapClassURI c :: IRI
c t :: Token
t = (SORT -> CASLFORMULA) -> Result SORT -> Result CASLFORMULA
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (PredType -> [TERM ()] -> SORT -> CASLFORMULA
forall f. PredType -> [TERM f] -> SORT -> FORMULA f
mkPred PredType
conceptPred [Token -> TERM ()
forall f. Token -> TERM f
mkThingVar Token
t]) (Result SORT -> Result CASLFORMULA)
-> Result SORT -> Result CASLFORMULA
forall a b. (a -> b) -> a -> b
$ IRI -> Result SORT
uriToIdM IRI
c

-- | Mapping of Individual URIs
mapIndivURI :: Individual -> Result (TERM ())
mapIndivURI :: IRI -> Result (TERM ())
mapIndivURI uriI :: IRI
uriI = do
    SORT
ur <- IRI -> Result SORT
uriToIdM IRI
uriI
    TERM () -> Result (TERM ())
forall (m :: * -> *) a. Monad m => a -> m a
return (TERM () -> Result (TERM ())) -> TERM () -> Result (TERM ())
forall a b. (a -> b) -> a -> b
$ OP_SYMB -> [TERM ()] -> TERM ()
forall f. OP_SYMB -> [TERM f] -> TERM f
mkAppl (SORT -> OP_TYPE -> OP_SYMB
mkQualOp SORT
ur (OpKind -> [SORT] -> SORT -> Range -> OP_TYPE
Op_type OpKind
Total [] SORT
thing Range
nullRange)) []

mapNNInt :: NNInt -> TERM ()
mapNNInt :: NNInt -> TERM ()
mapNNInt int :: NNInt
int = let NNInt uInt :: [Int]
uInt = NNInt
int in (TERM () -> TERM () -> TERM ()) -> [TERM ()] -> TERM ()
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 TERM () -> TERM () -> TERM ()
joinDigits ([TERM ()] -> TERM ()) -> [TERM ()] -> TERM ()
forall a b. (a -> b) -> a -> b
$ (Int -> TERM ()) -> [Int] -> [TERM ()]
forall a b. (a -> b) -> [a] -> [b]
map Int -> TERM ()
mkDigit [Int]
uInt

mapIntLit :: IntLit -> TERM ()
mapIntLit :: IntLit -> TERM ()
mapIntLit int :: IntLit
int =
    let cInt :: TERM ()
cInt = NNInt -> TERM ()
mapNNInt (NNInt -> TERM ()) -> NNInt -> TERM ()
forall a b. (a -> b) -> a -> b
$ IntLit -> NNInt
absInt IntLit
int
    in if IntLit -> Bool
isNegInt IntLit
int then TERM () -> TERM ()
negateInt (TERM () -> TERM ()) -> TERM () -> TERM ()
forall a b. (a -> b) -> a -> b
$ TERM () -> SORT -> TERM ()
upcast TERM ()
cInt SORT
integer
        else TERM () -> SORT -> TERM ()
upcast TERM ()
cInt SORT
integer

mapDecLit :: DecLit -> TERM ()
mapDecLit :: DecLit -> TERM ()
mapDecLit dec :: DecLit
dec =
    let ip :: IntLit
ip = DecLit -> IntLit
truncDec DecLit
dec
        np :: NNInt
np = IntLit -> NNInt
absInt IntLit
ip
        fp :: NNInt
fp = DecLit -> NNInt
fracDec DecLit
dec
        n :: TERM ()
n = TERM () -> TERM () -> TERM ()
mkDecimal (NNInt -> TERM ()
mapNNInt NNInt
np) (NNInt -> TERM ()
mapNNInt NNInt
fp)
    in if IntLit -> Bool
isNegInt IntLit
ip then TERM () -> TERM ()
negateFloat TERM ()
n else TERM ()
n

mapFloatLit :: FloatLit -> TERM ()
mapFloatLit :: FloatLit -> TERM ()
mapFloatLit f :: FloatLit
f =
    let fb :: DecLit
fb = FloatLit -> DecLit
floatBase FloatLit
f
        ex :: IntLit
ex = FloatLit -> IntLit
floatExp FloatLit
f
     in TERM () -> TERM () -> TERM ()
mkFloat (DecLit -> TERM ()
mapDecLit DecLit
fb) (IntLit -> TERM ()
mapIntLit IntLit
ex)

mapNrLit :: Literal -> TERM ()
mapNrLit :: Literal -> TERM ()
mapNrLit l :: Literal
l = case Literal
l of
    NumberLit f :: FloatLit
f
        | FloatLit -> Bool
isFloatInt FloatLit
f -> IntLit -> TERM ()
mapIntLit (IntLit -> TERM ()) -> IntLit -> TERM ()
forall a b. (a -> b) -> a -> b
$ DecLit -> IntLit
truncDec (DecLit -> IntLit) -> DecLit -> IntLit
forall a b. (a -> b) -> a -> b
$ FloatLit -> DecLit
floatBase FloatLit
f
        | FloatLit -> Bool
isFloatDec FloatLit
f -> DecLit -> TERM ()
mapDecLit (DecLit -> TERM ()) -> DecLit -> TERM ()
forall a b. (a -> b) -> a -> b
$ FloatLit -> DecLit
floatBase FloatLit
f
        | Bool
otherwise -> FloatLit -> TERM ()
mapFloatLit FloatLit
f
    _ -> String -> TERM ()
forall a. HasCallStack => String -> a
error "not number literal"

mapLiteral :: Literal -> Result (TERM ())
mapLiteral :: Literal -> Result (TERM ())
mapLiteral lit :: Literal
lit = TERM () -> Result (TERM ())
forall (m :: * -> *) a. Monad m => a -> m a
return (TERM () -> Result (TERM ())) -> TERM () -> Result (TERM ())
forall a b. (a -> b) -> a -> b
$ case Literal
lit of
    Literal l :: String
l ty :: TypedOrUntyped
ty -> TERM () -> SORT -> Range -> TERM ()
forall f. TERM f -> SORT -> Range -> TERM f
Sorted_term (case TypedOrUntyped
ty of
        Untyped _ -> (Char -> TERM () -> TERM ()) -> TERM () -> String -> TERM ()
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Char -> TERM () -> TERM ()
consChar TERM ()
emptyStringTerm String
l
        Typed dt :: IRI
dt -> case IRI -> DatatypeCat
getDatatypeCat IRI
dt of
            OWL2Number -> let p :: Either ParseError Literal
p = Parsec String () Literal
-> String -> String -> Either ParseError Literal
forall s t a.
Stream s Identity t =>
Parsec s () a -> String -> s -> Either ParseError a
parse Parsec String () Literal
forall st. CharParser st Literal
literal "" String
l in case Either ParseError Literal
p of
                Right nr :: Literal
nr -> Literal -> TERM ()
mapNrLit Literal
nr
                _ -> String -> TERM ()
forall a. HasCallStack => String -> a
error "cannot parse number literal"
            OWL2Bool -> case String
l of
                "true" -> TERM ()
trueT
                _ -> TERM ()
falseT
            _ -> (Char -> TERM () -> TERM ()) -> TERM () -> String -> TERM ()
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Char -> TERM () -> TERM ()
consChar TERM ()
emptyStringTerm String
l) SORT
dataS Range
nullRange
    _ -> Literal -> TERM ()
mapNrLit Literal
lit

-- | Mapping of data properties
mapDataProp :: DataPropertyExpression -> Int -> Int
            -> Result CASLFORMULA
mapDataProp :: IRI -> Int -> Int -> Result CASLFORMULA
mapDataProp dp :: IRI
dp a :: Int
a b :: Int
b = (SORT -> CASLFORMULA) -> Result SORT -> Result CASLFORMULA
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (PredType -> [TERM ()] -> SORT -> CASLFORMULA
forall f. PredType -> [TERM f] -> SORT -> FORMULA f
mkPred PredType
dataPropPred [Int -> TERM ()
forall f. Int -> TERM f
qualThing Int
a, Int -> TERM ()
forall f. Int -> TERM f
qualData Int
b])
    (Result SORT -> Result CASLFORMULA)
-> Result SORT -> Result CASLFORMULA
forall a b. (a -> b) -> a -> b
$ IRI -> Result SORT
uriToIdM IRI
dp

-- | Mapping of obj props
mapObjProp :: ObjectPropertyExpression -> Int -> Int
        -> Result CASLFORMULA
mapObjProp :: ObjectPropertyExpression -> Int -> Int -> Result CASLFORMULA
mapObjProp ob :: ObjectPropertyExpression
ob a :: Int
a b :: Int
b = case ObjectPropertyExpression
ob of
      ObjectProp u :: IRI
u -> (SORT -> CASLFORMULA) -> Result SORT -> Result CASLFORMULA
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (PredType -> [TERM ()] -> SORT -> CASLFORMULA
forall f. PredType -> [TERM f] -> SORT -> FORMULA f
mkPred PredType
objectPropPred ([TERM ()] -> SORT -> CASLFORMULA)
-> [TERM ()] -> SORT -> CASLFORMULA
forall a b. (a -> b) -> a -> b
$ (Int -> TERM ()) -> [Int] -> [TERM ()]
forall a b. (a -> b) -> [a] -> [b]
map Int -> TERM ()
forall f. Int -> TERM f
qualThing [Int
a, Int
b])
            (Result SORT -> Result CASLFORMULA)
-> Result SORT -> Result CASLFORMULA
forall a b. (a -> b) -> a -> b
$ IRI -> Result SORT
uriToIdM IRI
u
      ObjectInverseOf u :: ObjectPropertyExpression
u -> ObjectPropertyExpression -> Int -> Int -> Result CASLFORMULA
mapObjProp ObjectPropertyExpression
u Int
b Int
a

-- | Mapping of obj props with Individuals
mapObjPropI :: ObjectPropertyExpression -> VarOrIndi -> VarOrIndi
              -> Result CASLFORMULA
mapObjPropI :: ObjectPropertyExpression
-> VarOrIndi -> VarOrIndi -> Result CASLFORMULA
mapObjPropI ob :: ObjectPropertyExpression
ob lP :: VarOrIndi
lP rP :: VarOrIndi
rP = case ObjectPropertyExpression
ob of
    ObjectProp u :: IRI
u -> do
        TERM ()
l <- VarOrIndi -> Result (TERM ())
mapVar VarOrIndi
lP
        TERM ()
r <- VarOrIndi -> Result (TERM ())
mapVar VarOrIndi
rP
        (SORT -> CASLFORMULA) -> Result SORT -> Result CASLFORMULA
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (PredType -> [TERM ()] -> SORT -> CASLFORMULA
forall f. PredType -> [TERM f] -> SORT -> FORMULA f
mkPred PredType
objectPropPred [TERM ()
l, TERM ()
r]) (Result SORT -> Result CASLFORMULA)
-> Result SORT -> Result CASLFORMULA
forall a b. (a -> b) -> a -> b
$ IRI -> Result SORT
uriToIdM IRI
u
    ObjectInverseOf u :: ObjectPropertyExpression
u -> ObjectPropertyExpression
-> VarOrIndi -> VarOrIndi -> Result CASLFORMULA
mapObjPropI ObjectPropertyExpression
u VarOrIndi
rP VarOrIndi
lP

-- | mapping of individual list
mapComIndivList :: SameOrDifferent -> Maybe Individual
    -> [Individual] -> Result [CASLFORMULA]
mapComIndivList :: SameOrDifferent -> Maybe IRI -> [IRI] -> Result [CASLFORMULA]
mapComIndivList sod :: SameOrDifferent
sod mol :: Maybe IRI
mol inds :: [IRI]
inds = do
    [TERM ()]
fs <- (IRI -> Result (TERM ())) -> [IRI] -> Result [TERM ()]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM IRI -> Result (TERM ())
mapIndivURI [IRI]
inds
    [(TERM (), TERM ())]
tps <- case Maybe IRI
mol of
        Nothing -> [(TERM (), TERM ())] -> Result [(TERM (), TERM ())]
forall (m :: * -> *) a. Monad m => a -> m a
return ([(TERM (), TERM ())] -> Result [(TERM (), TERM ())])
-> [(TERM (), TERM ())] -> Result [(TERM (), TERM ())]
forall a b. (a -> b) -> a -> b
$ [TERM ()] -> [TERM ()] -> [(TERM (), TERM ())]
forall t t1. [t] -> [t1] -> [(t, t1)]
comPairs [TERM ()]
fs [TERM ()]
fs
        Just ol :: IRI
ol -> do
            TERM ()
f <- IRI -> Result (TERM ())
mapIndivURI IRI
ol
            [(TERM (), TERM ())] -> Result [(TERM (), TERM ())]
forall (m :: * -> *) a. Monad m => a -> m a
return ([(TERM (), TERM ())] -> Result [(TERM (), TERM ())])
-> [(TERM (), TERM ())] -> Result [(TERM (), TERM ())]
forall a b. (a -> b) -> a -> b
$ TERM () -> [TERM ()] -> [(TERM (), TERM ())]
forall t s. t -> [s] -> [(t, s)]
mkPairs TERM ()
f [TERM ()]
fs
    [CASLFORMULA] -> Result [CASLFORMULA]
forall (m :: * -> *) a. Monad m => a -> m a
return ([CASLFORMULA] -> Result [CASLFORMULA])
-> [CASLFORMULA] -> Result [CASLFORMULA]
forall a b. (a -> b) -> a -> b
$ ((TERM (), TERM ()) -> CASLFORMULA)
-> [(TERM (), TERM ())] -> [CASLFORMULA]
forall a b. (a -> b) -> [a] -> [b]
map (\ (x :: TERM ()
x, y :: TERM ()
y) -> case SameOrDifferent
sod of
        Same -> TERM () -> TERM () -> CASLFORMULA
forall f. TERM f -> TERM f -> FORMULA f
mkStEq TERM ()
x TERM ()
y
        Different -> CASLFORMULA -> CASLFORMULA
forall f. FORMULA f -> FORMULA f
mkNeg (CASLFORMULA -> CASLFORMULA) -> CASLFORMULA -> CASLFORMULA
forall a b. (a -> b) -> a -> b
$ TERM () -> TERM () -> CASLFORMULA
forall f. TERM f -> TERM f -> FORMULA f
mkStEq TERM ()
x TERM ()
y) [(TERM (), TERM ())]
tps

{- | Mapping along DataPropsList for creation of pairs for commutative
operations. -}
mapComDataPropsList :: Maybe DataPropertyExpression
    -> [DataPropertyExpression] -> Int -> Int
    -> Result [(CASLFORMULA, CASLFORMULA)]
mapComDataPropsList :: Maybe IRI
-> [IRI] -> Int -> Int -> Result [(CASLFORMULA, CASLFORMULA)]
mapComDataPropsList md :: Maybe IRI
md props :: [IRI]
props a :: Int
a b :: Int
b = do
    [CASLFORMULA]
fs <- (IRI -> Result CASLFORMULA) -> [IRI] -> Result [CASLFORMULA]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\ x :: IRI
x -> IRI -> Int -> Int -> Result CASLFORMULA
mapDataProp IRI
x Int
a Int
b) [IRI]
props
    case Maybe IRI
md of
        Nothing -> [(CASLFORMULA, CASLFORMULA)] -> Result [(CASLFORMULA, CASLFORMULA)]
forall (m :: * -> *) a. Monad m => a -> m a
return ([(CASLFORMULA, CASLFORMULA)]
 -> Result [(CASLFORMULA, CASLFORMULA)])
-> [(CASLFORMULA, CASLFORMULA)]
-> Result [(CASLFORMULA, CASLFORMULA)]
forall a b. (a -> b) -> a -> b
$ [CASLFORMULA] -> [CASLFORMULA] -> [(CASLFORMULA, CASLFORMULA)]
forall t t1. [t] -> [t1] -> [(t, t1)]
comPairs [CASLFORMULA]
fs [CASLFORMULA]
fs
        Just dp :: IRI
dp -> (CASLFORMULA -> [(CASLFORMULA, CASLFORMULA)])
-> Result CASLFORMULA -> Result [(CASLFORMULA, CASLFORMULA)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (CASLFORMULA -> [CASLFORMULA] -> [(CASLFORMULA, CASLFORMULA)]
forall t s. t -> [s] -> [(t, s)]
`mkPairs` [CASLFORMULA]
fs) (Result CASLFORMULA -> Result [(CASLFORMULA, CASLFORMULA)])
-> Result CASLFORMULA -> Result [(CASLFORMULA, CASLFORMULA)]
forall a b. (a -> b) -> a -> b
$ IRI -> Int -> Int -> Result CASLFORMULA
mapDataProp IRI
dp Int
a Int
b

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

mapDataRangeAux :: DataRange -> CASLTERM -> Result (CASLFORMULA, [CASLSign])
mapDataRangeAux :: DataRange -> TERM () -> Result (CASLFORMULA, [CASLSign])
mapDataRangeAux dr :: DataRange
dr i :: TERM ()
i = case DataRange
dr of
    DataType d :: IRI
d fl :: [(IRI, Literal)]
fl -> do
        let dt :: CASLFORMULA
dt = TERM () -> SORT -> CASLFORMULA
forall f. TERM f -> SORT -> FORMULA f
mkMember TERM ()
i (SORT -> CASLFORMULA) -> SORT -> CASLFORMULA
forall a b. (a -> b) -> a -> b
$ IRI -> SORT
uriToCaslId IRI
d 
        (sens :: [CASLFORMULA]
sens, s :: [[CASLSign]]
s) <- ((IRI, Literal) -> Result (CASLFORMULA, [CASLSign]))
-> [(IRI, Literal)] -> Result ([CASLFORMULA], [[CASLSign]])
forall (m :: * -> *) a b c.
Applicative m =>
(a -> m (b, c)) -> [a] -> m ([b], [c])
mapAndUnzipM (TERM () -> (IRI, Literal) -> Result (CASLFORMULA, [CASLSign])
mapFacet TERM ()
i) [(IRI, Literal)]
fl
        (CASLFORMULA, [CASLSign]) -> Result (CASLFORMULA, [CASLSign])
forall (m :: * -> *) a. Monad m => a -> m a
return ([CASLFORMULA] -> CASLFORMULA
forall f. [FORMULA f] -> FORMULA f
conjunct ([CASLFORMULA] -> CASLFORMULA) -> [CASLFORMULA] -> CASLFORMULA
forall a b. (a -> b) -> a -> b
$ CASLFORMULA
dt CASLFORMULA -> [CASLFORMULA] -> [CASLFORMULA]
forall a. a -> [a] -> [a]
: [CASLFORMULA]
sens, [[CASLSign]] -> [CASLSign]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[CASLSign]]
s)
    DataComplementOf drc :: DataRange
drc -> do
        (sens :: CASLFORMULA
sens, s :: [CASLSign]
s) <- DataRange -> TERM () -> Result (CASLFORMULA, [CASLSign])
mapDataRangeAux DataRange
drc TERM ()
i
        (CASLFORMULA, [CASLSign]) -> Result (CASLFORMULA, [CASLSign])
forall (m :: * -> *) a. Monad m => a -> m a
return (CASLFORMULA -> CASLFORMULA
forall f. FORMULA f -> FORMULA f
mkNeg CASLFORMULA
sens, [CASLSign]
s)
    DataJunction jt :: JunctionType
jt drl :: [DataRange]
drl -> do
        (jl :: [CASLFORMULA]
jl, sl :: [[CASLSign]]
sl) <- (DataRange -> Result (CASLFORMULA, [CASLSign]))
-> [DataRange] -> Result ([CASLFORMULA], [[CASLSign]])
forall (m :: * -> *) a b c.
Applicative m =>
(a -> m (b, c)) -> [a] -> m ([b], [c])
mapAndUnzipM ((\ v :: TERM ()
v r :: DataRange
r -> DataRange -> TERM () -> Result (CASLFORMULA, [CASLSign])
mapDataRangeAux DataRange
r TERM ()
v) TERM ()
i) [DataRange]
drl
        --let usig = uniteL sl
        (CASLFORMULA, [CASLSign]) -> Result (CASLFORMULA, [CASLSign])
forall (m :: * -> *) a. Monad m => a -> m a
return ((CASLFORMULA, [CASLSign]) -> Result (CASLFORMULA, [CASLSign]))
-> (CASLFORMULA, [CASLSign]) -> Result (CASLFORMULA, [CASLSign])
forall a b. (a -> b) -> a -> b
$ case JunctionType
jt of
                IntersectionOf -> ([CASLFORMULA] -> CASLFORMULA
forall f. [FORMULA f] -> FORMULA f
conjunct [CASLFORMULA]
jl, [[CASLSign]] -> [CASLSign]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[CASLSign]]
sl)
                UnionOf -> ([CASLFORMULA] -> CASLFORMULA
forall f. [FORMULA f] -> FORMULA f
disjunct [CASLFORMULA]
jl, [[CASLSign]] -> [CASLSign]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[CASLSign]]
sl)
    DataOneOf cs :: [Literal]
cs -> do
        [TERM ()]
ls <- (Literal -> Result (TERM ())) -> [Literal] -> Result [TERM ()]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Literal -> Result (TERM ())
mapLiteral [Literal]
cs
        (CASLFORMULA, [CASLSign]) -> Result (CASLFORMULA, [CASLSign])
forall (m :: * -> *) a. Monad m => a -> m a
return ([CASLFORMULA] -> CASLFORMULA
forall f. [FORMULA f] -> FORMULA f
disjunct ([CASLFORMULA] -> CASLFORMULA) -> [CASLFORMULA] -> CASLFORMULA
forall a b. (a -> b) -> a -> b
$ (TERM () -> CASLFORMULA) -> [TERM ()] -> [CASLFORMULA]
forall a b. (a -> b) -> [a] -> [b]
map (TERM () -> TERM () -> CASLFORMULA
forall f. TERM f -> TERM f -> FORMULA f
mkStEq TERM ()
i) [TERM ()]
ls, [])

-- | mapping of Data Range
mapDataRange :: DataRange -> Int -> Result (CASLFORMULA, [CASLSign])
mapDataRange :: DataRange -> Int -> Result (CASLFORMULA, [CASLSign])
mapDataRange dr :: DataRange
dr = DataRange -> TERM () -> Result (CASLFORMULA, [CASLSign])
mapDataRangeAux DataRange
dr (TERM () -> Result (CASLFORMULA, [CASLSign]))
-> (Int -> TERM ()) -> Int -> Result (CASLFORMULA, [CASLSign])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> TERM ()
forall f. Int -> TERM f
qualData

mkFacetPred :: TERM f -> ConstrainingFacet -> TERM f -> (FORMULA f, Id)
mkFacetPred :: TERM f -> IRI -> TERM f -> (FORMULA f, SORT)
mkFacetPred lit :: TERM f
lit f :: IRI
f var :: TERM f
var =
    let cf :: SORT
cf = String -> SORT
mkInfix (String -> SORT) -> String -> SORT
forall a b. (a -> b) -> a -> b
$ IRI -> String
fromCF IRI
f
    in (PredType -> [TERM f] -> SORT -> FORMULA f
forall f. PredType -> [TERM f] -> SORT -> FORMULA f
mkPred PredType
dataPred [TERM f
var, TERM f
lit] SORT
cf, SORT
cf)

mapFacet :: CASLTERM -> (ConstrainingFacet, RestrictionValue)
    -> Result (CASLFORMULA, [CASLSign])
mapFacet :: TERM () -> (IRI, Literal) -> Result (CASLFORMULA, [CASLSign])
mapFacet var :: TERM ()
var (f :: IRI
f, r :: Literal
r) = do
    TERM ()
con <- Literal -> Result (TERM ())
mapLiteral Literal
r
    let (fp :: CASLFORMULA
fp, cf :: SORT
cf) = TERM () -> IRI -> TERM () -> (CASLFORMULA, SORT)
forall f. TERM f -> IRI -> TERM f -> (FORMULA f, SORT)
mkFacetPred TERM ()
con IRI
f TERM ()
var
    (CASLFORMULA, [CASLSign]) -> Result (CASLFORMULA, [CASLSign])
forall (m :: * -> *) a. Monad m => a -> m a
return (CASLFORMULA
fp, 
            [(() -> CASLSign
forall e f. e -> Sign f e
emptySign ()) {predMap :: MapSet SORT PredType
predMap = [(SORT, [PredType])] -> MapSet SORT PredType
forall a b. (Ord a, Ord b) => [(a, [b])] -> MapSet a b
MapSet.fromList [(SORT
cf, [PredType
dataPred])]}])

cardProps :: Bool
    -> Either ObjectPropertyExpression DataPropertyExpression -> Int
    -> [Int] -> Result [CASLFORMULA]
cardProps :: Bool
-> Either ObjectPropertyExpression IRI
-> Int
-> [Int]
-> Result [CASLFORMULA]
cardProps b :: Bool
b prop :: Either ObjectPropertyExpression IRI
prop var :: Int
var vLst :: [Int]
vLst =
    if Bool
b then let Left ope :: ObjectPropertyExpression
ope = Either ObjectPropertyExpression IRI
prop in (Int -> Result CASLFORMULA) -> [Int] -> Result [CASLFORMULA]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (ObjectPropertyExpression -> Int -> Int -> Result CASLFORMULA
mapObjProp ObjectPropertyExpression
ope Int
var) [Int]
vLst
     else let Right dpe :: IRI
dpe = Either ObjectPropertyExpression IRI
prop in (Int -> Result CASLFORMULA) -> [Int] -> Result [CASLFORMULA]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (IRI -> Int -> Int -> Result CASLFORMULA
mapDataProp IRI
dpe Int
var) [Int]
vLst

mapCard :: Bool -> CardinalityType -> Int
    -> Either ObjectPropertyExpression DataPropertyExpression
    -> Maybe (Either ClassExpression DataRange) -> Int
    -> Result (FORMULA (), [CASLSign])
mapCard :: Bool
-> CardinalityType
-> Int
-> Either ObjectPropertyExpression IRI
-> Maybe (Either ClassExpression DataRange)
-> Int
-> Result (CASLFORMULA, [CASLSign])
mapCard b :: Bool
b ct :: CardinalityType
ct n :: Int
n prop :: Either ObjectPropertyExpression IRI
prop d :: Maybe (Either ClassExpression DataRange)
d var :: Int
var = do
    let vlst :: [Int]
vlst = (Int -> Int) -> [Int] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map (Int
var Int -> Int -> Int
forall a. Num a => a -> a -> a
+) [1 .. Int
n]
        vlstM :: [Int]
vlstM = [Int]
vlst [Int] -> [Int] -> [Int]
forall a. [a] -> [a] -> [a]
++ [Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
var Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1]
        vlstE :: [Int]
vlstE = [Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
var Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1]
    (dOut :: [CASLFORMULA]
dOut, s :: [[CASLSign]]
s) <- case Maybe (Either ClassExpression DataRange)
d of
        Nothing -> ([CASLFORMULA], [[CASLSign]])
-> Result ([CASLFORMULA], [[CASLSign]])
forall (m :: * -> *) a. Monad m => a -> m a
return ([], [])
        Just y :: Either ClassExpression DataRange
y ->
           if Bool
b then let Left ce :: ClassExpression
ce = Either ClassExpression DataRange
y in (Int -> Result (CASLFORMULA, [CASLSign]))
-> [Int] -> Result ([CASLFORMULA], [[CASLSign]])
forall (m :: * -> *) a b c.
Applicative m =>
(a -> m (b, c)) -> [a] -> m ([b], [c])
mapAndUnzipM
                        (ClassExpression -> Int -> Result (CASLFORMULA, [CASLSign])
mapDescription ClassExpression
ce) [Int]
vlst
           else let Right dr :: DataRange
dr = Either ClassExpression DataRange
y in (Int -> Result (CASLFORMULA, [CASLSign]))
-> [Int] -> Result ([CASLFORMULA], [[CASLSign]])
forall (m :: * -> *) a b c.
Applicative m =>
(a -> m (b, c)) -> [a] -> m ([b], [c])
mapAndUnzipM (DataRange -> Int -> Result (CASLFORMULA, [CASLSign])
mapDataRange DataRange
dr) [Int]
vlst
    (eOut :: [CASLFORMULA]
eOut, s' :: [[CASLSign]]
s') <- case Maybe (Either ClassExpression DataRange)
d of
        Nothing -> ([CASLFORMULA], [[CASLSign]])
-> Result ([CASLFORMULA], [[CASLSign]])
forall (m :: * -> *) a. Monad m => a -> m a
return ([], [])
        Just y :: Either ClassExpression DataRange
y ->
           if Bool
b then let Left ce :: ClassExpression
ce = Either ClassExpression DataRange
y in (Int -> Result (CASLFORMULA, [CASLSign]))
-> [Int] -> Result ([CASLFORMULA], [[CASLSign]])
forall (m :: * -> *) a b c.
Applicative m =>
(a -> m (b, c)) -> [a] -> m ([b], [c])
mapAndUnzipM
                        (ClassExpression -> Int -> Result (CASLFORMULA, [CASLSign])
mapDescription ClassExpression
ce) [Int]
vlstM
           else let Right dr :: DataRange
dr = Either ClassExpression DataRange
y in (Int -> Result (CASLFORMULA, [CASLSign]))
-> [Int] -> Result ([CASLFORMULA], [[CASLSign]])
forall (m :: * -> *) a b c.
Applicative m =>
(a -> m (b, c)) -> [a] -> m ([b], [c])
mapAndUnzipM (DataRange -> Int -> Result (CASLFORMULA, [CASLSign])
mapDataRange DataRange
dr) [Int]
vlstM
    (fOut :: [CASLFORMULA]
fOut, s'' :: [[CASLSign]]
s'') <- case Maybe (Either ClassExpression DataRange)
d of
        Nothing -> ([CASLFORMULA], [[CASLSign]])
-> Result ([CASLFORMULA], [[CASLSign]])
forall (m :: * -> *) a. Monad m => a -> m a
return ([], [])
        Just y :: Either ClassExpression DataRange
y ->
           if Bool
b then let Left ce :: ClassExpression
ce = Either ClassExpression DataRange
y in (Int -> Result (CASLFORMULA, [CASLSign]))
-> [Int] -> Result ([CASLFORMULA], [[CASLSign]])
forall (m :: * -> *) a b c.
Applicative m =>
(a -> m (b, c)) -> [a] -> m ([b], [c])
mapAndUnzipM
                        (ClassExpression -> Int -> Result (CASLFORMULA, [CASLSign])
mapDescription ClassExpression
ce) [Int]
vlstE
           else let Right dr :: DataRange
dr = Either ClassExpression DataRange
y in (Int -> Result (CASLFORMULA, [CASLSign]))
-> [Int] -> Result ([CASLFORMULA], [[CASLSign]])
forall (m :: * -> *) a b c.
Applicative m =>
(a -> m (b, c)) -> [a] -> m ([b], [c])
mapAndUnzipM (DataRange -> Int -> Result (CASLFORMULA, [CASLSign])
mapDataRange DataRange
dr) [Int]
vlstE
    let dlst :: [FORMULA f]
dlst = ((Int, Int) -> FORMULA f) -> [(Int, Int)] -> [FORMULA f]
forall a b. (a -> b) -> [a] -> [b]
map (\ (x :: Int
x, y :: Int
y) -> FORMULA f -> FORMULA f
forall f. FORMULA f -> FORMULA f
mkNeg (FORMULA f -> FORMULA f) -> FORMULA f -> FORMULA f
forall a b. (a -> b) -> a -> b
$ TERM f -> TERM f -> FORMULA f
forall f. TERM f -> TERM f -> FORMULA f
mkStEq (Int -> TERM f
forall f. Int -> TERM f
qualThing Int
x) (TERM f -> FORMULA f) -> TERM f -> FORMULA f
forall a b. (a -> b) -> a -> b
$ Int -> TERM f
forall f. Int -> TERM f
qualThing Int
y)
                        ([(Int, Int)] -> [FORMULA f]) -> [(Int, Int)] -> [FORMULA f]
forall a b. (a -> b) -> a -> b
$ [Int] -> [Int] -> [(Int, Int)]
forall t t1. [t] -> [t1] -> [(t, t1)]
comPairs [Int]
vlst [Int]
vlst
        dlstM :: [FORMULA f]
dlstM = ((Int, Int) -> FORMULA f) -> [(Int, Int)] -> [FORMULA f]
forall a b. (a -> b) -> [a] -> [b]
map (\ (x :: Int
x, y :: Int
y) -> TERM f -> TERM f -> FORMULA f
forall f. TERM f -> TERM f -> FORMULA f
mkStEq (Int -> TERM f
forall f. Int -> TERM f
qualThing Int
x) (TERM f -> FORMULA f) -> TERM f -> FORMULA f
forall a b. (a -> b) -> a -> b
$ Int -> TERM f
forall f. Int -> TERM f
qualThing Int
y)
                        ([(Int, Int)] -> [FORMULA f]) -> [(Int, Int)] -> [FORMULA f]
forall a b. (a -> b) -> a -> b
$ [Int] -> [Int] -> [(Int, Int)]
forall t t1. [t] -> [t1] -> [(t, t1)]
comPairs [Int]
vlstM [Int]
vlstM
        qVars :: [VAR_DECL]
qVars = (Int -> VAR_DECL) -> [Int] -> [VAR_DECL]
forall a b. (a -> b) -> [a] -> [b]
map Int -> VAR_DECL
thingDecl [Int]
vlst
        qVarsM :: [VAR_DECL]
qVarsM = (Int -> VAR_DECL) -> [Int] -> [VAR_DECL]
forall a b. (a -> b) -> [a] -> [b]
map Int -> VAR_DECL
thingDecl [Int]
vlstM
        qVarsE :: [VAR_DECL]
qVarsE = (Int -> VAR_DECL) -> [Int] -> [VAR_DECL]
forall a b. (a -> b) -> [a] -> [b]
map Int -> VAR_DECL
thingDecl [Int]
vlstE
    [CASLFORMULA]
oProps <- Bool
-> Either ObjectPropertyExpression IRI
-> Int
-> [Int]
-> Result [CASLFORMULA]
cardProps Bool
b Either ObjectPropertyExpression IRI
prop Int
var [Int]
vlst
    [CASLFORMULA]
oPropsM <- Bool
-> Either ObjectPropertyExpression IRI
-> Int
-> [Int]
-> Result [CASLFORMULA]
cardProps Bool
b Either ObjectPropertyExpression IRI
prop Int
var [Int]
vlstM
    [CASLFORMULA]
oPropsE <- Bool
-> Either ObjectPropertyExpression IRI
-> Int
-> [Int]
-> Result [CASLFORMULA]
cardProps Bool
b Either ObjectPropertyExpression IRI
prop Int
var [Int]
vlstE
    let minLst :: CASLFORMULA
minLst = [CASLFORMULA] -> CASLFORMULA
forall f. [FORMULA f] -> FORMULA f
conjunct ([CASLFORMULA] -> CASLFORMULA) -> [CASLFORMULA] -> CASLFORMULA
forall a b. (a -> b) -> a -> b
$ [CASLFORMULA]
forall f. [FORMULA f]
dlst [CASLFORMULA] -> [CASLFORMULA] -> [CASLFORMULA]
forall a. [a] -> [a] -> [a]
++ [CASLFORMULA]
oProps [CASLFORMULA] -> [CASLFORMULA] -> [CASLFORMULA]
forall a. [a] -> [a] -> [a]
++ [CASLFORMULA]
dOut
        maxLst :: CASLFORMULA
maxLst = CASLFORMULA -> CASLFORMULA -> CASLFORMULA
forall f. FORMULA f -> FORMULA f -> FORMULA f
mkImpl ([CASLFORMULA] -> CASLFORMULA
forall f. [FORMULA f] -> FORMULA f
conjunct ([CASLFORMULA] -> CASLFORMULA) -> [CASLFORMULA] -> CASLFORMULA
forall a b. (a -> b) -> a -> b
$ [CASLFORMULA]
oPropsM [CASLFORMULA] -> [CASLFORMULA] -> [CASLFORMULA]
forall a. [a] -> [a] -> [a]
++ [CASLFORMULA]
eOut)
                        (CASLFORMULA -> CASLFORMULA) -> CASLFORMULA -> CASLFORMULA
forall a b. (a -> b) -> a -> b
$ [CASLFORMULA] -> CASLFORMULA
forall f. [FORMULA f] -> FORMULA f
disjunct [CASLFORMULA]
forall f. [FORMULA f]
dlstM
        exactLst' :: CASLFORMULA
exactLst' = CASLFORMULA -> CASLFORMULA -> CASLFORMULA
forall f. FORMULA f -> FORMULA f -> FORMULA f
mkImpl ([CASLFORMULA] -> CASLFORMULA
forall f. [FORMULA f] -> FORMULA f
conjunct ([CASLFORMULA] -> CASLFORMULA) -> [CASLFORMULA] -> CASLFORMULA
forall a b. (a -> b) -> a -> b
$ [CASLFORMULA]
oPropsE [CASLFORMULA] -> [CASLFORMULA] -> [CASLFORMULA]
forall a. [a] -> [a] -> [a]
++ [CASLFORMULA]
fOut) (CASLFORMULA -> CASLFORMULA) -> CASLFORMULA -> CASLFORMULA
forall a b. (a -> b) -> a -> b
$ [CASLFORMULA] -> CASLFORMULA
forall f. [FORMULA f] -> FORMULA f
disjunct [CASLFORMULA]
forall f. [FORMULA f]
dlstM
        senAux :: CASLFORMULA
senAux = [CASLFORMULA] -> CASLFORMULA
forall f. [FORMULA f] -> FORMULA f
conjunct [CASLFORMULA
minLst, [VAR_DECL] -> CASLFORMULA -> CASLFORMULA
forall f. [VAR_DECL] -> FORMULA f -> FORMULA f
mkForall [VAR_DECL]
qVarsE CASLFORMULA
exactLst']
        exactLst :: CASLFORMULA
exactLst =  if [VAR_DECL] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [VAR_DECL]
qVars then CASLFORMULA
senAux else [VAR_DECL] -> CASLFORMULA -> CASLFORMULA
forall f. [VAR_DECL] -> FORMULA f -> FORMULA f
mkExist [VAR_DECL]
qVars CASLFORMULA
senAux
        ts :: [CASLSign]
ts = [[CASLSign]] -> [CASLSign]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[CASLSign]] -> [CASLSign]) -> [[CASLSign]] -> [CASLSign]
forall a b. (a -> b) -> a -> b
$ [[CASLSign]]
s [[CASLSign]] -> [[CASLSign]] -> [[CASLSign]]
forall a. [a] -> [a] -> [a]
++ [[CASLSign]]
s' [[CASLSign]] -> [[CASLSign]] -> [[CASLSign]]
forall a. [a] -> [a] -> [a]
++ [[CASLSign]]
s''
    (CASLFORMULA, [CASLSign]) -> Result (CASLFORMULA, [CASLSign])
forall (m :: * -> *) a. Monad m => a -> m a
return ((CASLFORMULA, [CASLSign]) -> Result (CASLFORMULA, [CASLSign]))
-> (CASLFORMULA, [CASLSign]) -> Result (CASLFORMULA, [CASLSign])
forall a b. (a -> b) -> a -> b
$ case CardinalityType
ct of
            MinCardinality -> ([VAR_DECL] -> CASLFORMULA -> CASLFORMULA
forall f. [VAR_DECL] -> FORMULA f -> FORMULA f
mkExist [VAR_DECL]
qVars CASLFORMULA
minLst, [CASLSign]
ts)
            MaxCardinality -> ([VAR_DECL] -> CASLFORMULA -> CASLFORMULA
forall f. [VAR_DECL] -> FORMULA f -> FORMULA f
mkForall [VAR_DECL]
qVarsM CASLFORMULA
maxLst, [CASLSign]
ts)
            ExactCardinality -> (CASLFORMULA
exactLst, [CASLSign]
ts)

-- | mapping of OWL2 Descriptions
mapDescription :: ClassExpression -> Int ->
    Result (CASLFORMULA, [CASLSign])
mapDescription :: ClassExpression -> Int -> Result (CASLFORMULA, [CASLSign])
mapDescription desc :: ClassExpression
desc var :: Int
var = case ClassExpression
desc of
    Expression u :: IRI
u -> do
        CASLFORMULA
c <- IRI -> Token -> Result CASLFORMULA
mapClassURI IRI
u (Token -> Result CASLFORMULA) -> Token -> Result CASLFORMULA
forall a b. (a -> b) -> a -> b
$ Int -> Token
mkNName Int
var
        (CASLFORMULA, [CASLSign]) -> Result (CASLFORMULA, [CASLSign])
forall (m :: * -> *) a. Monad m => a -> m a
return (CASLFORMULA
c, [])
    ObjectJunction ty :: JunctionType
ty ds :: [ClassExpression]
ds -> do
        (els :: [CASLFORMULA]
els, s :: [[CASLSign]]
s) <- (ClassExpression -> Result (CASLFORMULA, [CASLSign]))
-> [ClassExpression] -> Result ([CASLFORMULA], [[CASLSign]])
forall (m :: * -> *) a b c.
Applicative m =>
(a -> m (b, c)) -> [a] -> m ([b], [c])
mapAndUnzipM ((ClassExpression -> Int -> Result (CASLFORMULA, [CASLSign]))
-> Int -> ClassExpression -> Result (CASLFORMULA, [CASLSign])
forall a b c. (a -> b -> c) -> b -> a -> c
flip ClassExpression -> Int -> Result (CASLFORMULA, [CASLSign])
mapDescription Int
var) [ClassExpression]
ds
        (CASLFORMULA, [CASLSign]) -> Result (CASLFORMULA, [CASLSign])
forall (m :: * -> *) a. Monad m => a -> m a
return ((case JunctionType
ty of
                UnionOf -> [CASLFORMULA] -> CASLFORMULA
forall f. [FORMULA f] -> FORMULA f
disjunct
                IntersectionOf -> [CASLFORMULA] -> CASLFORMULA
forall f. [FORMULA f] -> FORMULA f
conjunct)
            [CASLFORMULA]
els, [[CASLSign]] -> [CASLSign]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[CASLSign]]
s)
    ObjectComplementOf d :: ClassExpression
d -> do
        (els :: CASLFORMULA
els, s :: [CASLSign]
s) <- ClassExpression -> Int -> Result (CASLFORMULA, [CASLSign])
mapDescription ClassExpression
d Int
var
        (CASLFORMULA, [CASLSign]) -> Result (CASLFORMULA, [CASLSign])
forall (m :: * -> *) a. Monad m => a -> m a
return (CASLFORMULA -> CASLFORMULA
forall f. FORMULA f -> FORMULA f
mkNeg CASLFORMULA
els, [CASLSign]
s)
    ObjectOneOf is :: [IRI]
is -> do
        [TERM ()]
il <- (IRI -> Result (TERM ())) -> [IRI] -> Result [TERM ()]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM IRI -> Result (TERM ())
mapIndivURI [IRI]
is
        (CASLFORMULA, [CASLSign]) -> Result (CASLFORMULA, [CASLSign])
forall (m :: * -> *) a. Monad m => a -> m a
return ([CASLFORMULA] -> CASLFORMULA
forall f. [FORMULA f] -> FORMULA f
disjunct ([CASLFORMULA] -> CASLFORMULA) -> [CASLFORMULA] -> CASLFORMULA
forall a b. (a -> b) -> a -> b
$ (TERM () -> CASLFORMULA) -> [TERM ()] -> [CASLFORMULA]
forall a b. (a -> b) -> [a] -> [b]
map (TERM () -> TERM () -> CASLFORMULA
forall f. TERM f -> TERM f -> FORMULA f
mkStEq (TERM () -> TERM () -> CASLFORMULA)
-> TERM () -> TERM () -> CASLFORMULA
forall a b. (a -> b) -> a -> b
$ Int -> TERM ()
forall f. Int -> TERM f
qualThing Int
var) [TERM ()]
il, [])
    ObjectValuesFrom ty :: QuantifierType
ty o :: ObjectPropertyExpression
o d :: ClassExpression
d -> let n :: Int
n = Int
var Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1 in do
        CASLFORMULA
oprop0 <- ObjectPropertyExpression -> Int -> Int -> Result CASLFORMULA
mapObjProp ObjectPropertyExpression
o Int
var Int
n
        (desc0 :: CASLFORMULA
desc0, s :: [CASLSign]
s) <- ClassExpression -> Int -> Result (CASLFORMULA, [CASLSign])
mapDescription ClassExpression
d Int
n
        (CASLFORMULA, [CASLSign]) -> Result (CASLFORMULA, [CASLSign])
forall (m :: * -> *) a. Monad m => a -> m a
return ((CASLFORMULA, [CASLSign]) -> Result (CASLFORMULA, [CASLSign]))
-> (CASLFORMULA, [CASLSign]) -> Result (CASLFORMULA, [CASLSign])
forall a b. (a -> b) -> a -> b
$ case QuantifierType
ty of
            SomeValuesFrom -> ([VAR_DECL] -> CASLFORMULA -> CASLFORMULA
forall f. [VAR_DECL] -> FORMULA f -> FORMULA f
mkExist [Int -> VAR_DECL
thingDecl Int
n] (CASLFORMULA -> CASLFORMULA) -> CASLFORMULA -> CASLFORMULA
forall a b. (a -> b) -> a -> b
$ [CASLFORMULA] -> CASLFORMULA
forall f. [FORMULA f] -> FORMULA f
conjunct [CASLFORMULA
oprop0, CASLFORMULA
desc0],
                               [CASLSign]
s)
            AllValuesFrom -> ([Int] -> CASLFORMULA -> CASLFORMULA
forall f. [Int] -> FORMULA f -> FORMULA f
mkVDecl [Int
n] (CASLFORMULA -> CASLFORMULA) -> CASLFORMULA -> CASLFORMULA
forall a b. (a -> b) -> a -> b
$ CASLFORMULA -> CASLFORMULA -> CASLFORMULA
forall f. FORMULA f -> FORMULA f -> FORMULA f
mkImpl CASLFORMULA
oprop0 CASLFORMULA
desc0,
                               [CASLSign]
s)
    ObjectHasSelf o :: ObjectPropertyExpression
o -> do
        CASLFORMULA
op <- ObjectPropertyExpression -> Int -> Int -> Result CASLFORMULA
mapObjProp ObjectPropertyExpression
o Int
var Int
var
        (CASLFORMULA, [CASLSign]) -> Result (CASLFORMULA, [CASLSign])
forall (m :: * -> *) a. Monad m => a -> m a
return (CASLFORMULA
op, [])
    ObjectHasValue o :: ObjectPropertyExpression
o i :: IRI
i -> do
        CASLFORMULA
op <- ObjectPropertyExpression
-> VarOrIndi -> VarOrIndi -> Result CASLFORMULA
mapObjPropI ObjectPropertyExpression
o (Int -> VarOrIndi
OVar Int
var) (IRI -> VarOrIndi
OIndi IRI
i)
        (CASLFORMULA, [CASLSign]) -> Result (CASLFORMULA, [CASLSign])
forall (m :: * -> *) a. Monad m => a -> m a
return (CASLFORMULA
op, [])
    ObjectCardinality (Cardinality ct :: CardinalityType
ct n :: Int
n oprop :: ObjectPropertyExpression
oprop d :: Maybe ClassExpression
d) -> Bool
-> CardinalityType
-> Int
-> Either ObjectPropertyExpression IRI
-> Maybe (Either ClassExpression DataRange)
-> Int
-> Result (CASLFORMULA, [CASLSign])
mapCard Bool
True CardinalityType
ct Int
n
        (ObjectPropertyExpression -> Either ObjectPropertyExpression IRI
forall a b. a -> Either a b
Left ObjectPropertyExpression
oprop) ((ClassExpression -> Either ClassExpression DataRange)
-> Maybe ClassExpression
-> Maybe (Either ClassExpression DataRange)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ClassExpression -> Either ClassExpression DataRange
forall a b. a -> Either a b
Left Maybe ClassExpression
d) Int
var
    DataValuesFrom ty :: QuantifierType
ty dpe :: [IRI]
dpe dr :: DataRange
dr -> let n :: Int
n = Int
var Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1 in do
        CASLFORMULA
oprop0 <- IRI -> Int -> Int -> Result CASLFORMULA
mapDataProp ([IRI] -> IRI
forall a. [a] -> a
head [IRI]
dpe) Int
var Int
n
        (desc0 :: CASLFORMULA
desc0, s :: [CASLSign]
s) <- DataRange -> Int -> Result (CASLFORMULA, [CASLSign])
mapDataRange DataRange
dr Int
n
        --let ts = niteCASLSign cSig s
        (CASLFORMULA, [CASLSign]) -> Result (CASLFORMULA, [CASLSign])
forall (m :: * -> *) a. Monad m => a -> m a
return ((CASLFORMULA, [CASLSign]) -> Result (CASLFORMULA, [CASLSign]))
-> (CASLFORMULA, [CASLSign]) -> Result (CASLFORMULA, [CASLSign])
forall a b. (a -> b) -> a -> b
$ case QuantifierType
ty of
            SomeValuesFrom -> ([VAR_DECL] -> CASLFORMULA -> CASLFORMULA
forall f. [VAR_DECL] -> FORMULA f -> FORMULA f
mkExist [Int -> VAR_DECL
dataDecl Int
n] (CASLFORMULA -> CASLFORMULA) -> CASLFORMULA -> CASLFORMULA
forall a b. (a -> b) -> a -> b
$ [CASLFORMULA] -> CASLFORMULA
forall f. [FORMULA f] -> FORMULA f
conjunct [CASLFORMULA
oprop0, CASLFORMULA
desc0],
                [CASLSign]
s)
            AllValuesFrom -> ([Int] -> CASLFORMULA -> CASLFORMULA
forall f. [Int] -> FORMULA f -> FORMULA f
mkVDataDecl [Int
n] (CASLFORMULA -> CASLFORMULA) -> CASLFORMULA -> CASLFORMULA
forall a b. (a -> b) -> a -> b
$ CASLFORMULA -> CASLFORMULA -> CASLFORMULA
forall f. FORMULA f -> FORMULA f -> FORMULA f
mkImpl CASLFORMULA
oprop0 CASLFORMULA
desc0, [CASLSign]
s)
    DataHasValue dpe :: IRI
dpe c :: Literal
c -> do
        TERM ()
con <- Literal -> Result (TERM ())
mapLiteral Literal
c
        (CASLFORMULA, [CASLSign]) -> Result (CASLFORMULA, [CASLSign])
forall (m :: * -> *) a. Monad m => a -> m a
return (PredType -> [TERM ()] -> SORT -> CASLFORMULA
forall f. PredType -> [TERM f] -> SORT -> FORMULA f
mkPred PredType
dataPropPred [Int -> TERM ()
forall f. Int -> TERM f
qualThing Int
var, TERM ()
con]
                           (SORT -> CASLFORMULA) -> SORT -> CASLFORMULA
forall a b. (a -> b) -> a -> b
$ IRI -> SORT
uriToCaslId IRI
dpe, [])
    DataCardinality (Cardinality ct :: CardinalityType
ct n :: Int
n dpe :: IRI
dpe dr :: Maybe DataRange
dr) -> Bool
-> CardinalityType
-> Int
-> Either ObjectPropertyExpression IRI
-> Maybe (Either ClassExpression DataRange)
-> Int
-> Result (CASLFORMULA, [CASLSign])
mapCard Bool
False CardinalityType
ct Int
n
        (IRI -> Either ObjectPropertyExpression IRI
forall a b. b -> Either a b
Right IRI
dpe) ((DataRange -> Either ClassExpression DataRange)
-> Maybe DataRange -> Maybe (Either ClassExpression DataRange)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap DataRange -> Either ClassExpression DataRange
forall a b. b -> Either a b
Right Maybe DataRange
dr) Int
var

-- | Mapping of a list of descriptions
mapDescriptionList :: Int -> [ClassExpression]
        -> Result ([CASLFORMULA], [CASLSign])
mapDescriptionList :: Int -> [ClassExpression] -> Result ([CASLFORMULA], [CASLSign])
mapDescriptionList n :: Int
n lst :: [ClassExpression]
lst = do
    (els :: [CASLFORMULA]
els, s :: [[CASLSign]]
s) <- ((ClassExpression, Int) -> Result (CASLFORMULA, [CASLSign]))
-> [(ClassExpression, Int)] -> Result ([CASLFORMULA], [[CASLSign]])
forall (m :: * -> *) a b c.
Applicative m =>
(a -> m (b, c)) -> [a] -> m ([b], [c])
mapAndUnzipM ((ClassExpression -> Int -> Result (CASLFORMULA, [CASLSign]))
-> (ClassExpression, Int) -> Result (CASLFORMULA, [CASLSign])
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry ((ClassExpression -> Int -> Result (CASLFORMULA, [CASLSign]))
 -> (ClassExpression, Int) -> Result (CASLFORMULA, [CASLSign]))
-> (ClassExpression -> Int -> Result (CASLFORMULA, [CASLSign]))
-> (ClassExpression, Int)
-> Result (CASLFORMULA, [CASLSign])
forall a b. (a -> b) -> a -> b
$ ClassExpression -> Int -> Result (CASLFORMULA, [CASLSign])
mapDescription)
                    ([(ClassExpression, Int)] -> Result ([CASLFORMULA], [[CASLSign]]))
-> [(ClassExpression, Int)] -> Result ([CASLFORMULA], [[CASLSign]])
forall a b. (a -> b) -> a -> b
$ [ClassExpression] -> [Int] -> [(ClassExpression, Int)]
forall t t1. [t] -> [t1] -> [(t, t1)]
zip [ClassExpression]
lst ([Int] -> [(ClassExpression, Int)])
-> [Int] -> [(ClassExpression, Int)]
forall a b. (a -> b) -> a -> b
$ Int -> Int -> [Int]
forall a. Int -> a -> [a]
replicate ([ClassExpression] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [ClassExpression]
lst) Int
n
    ([CASLFORMULA], [CASLSign]) -> Result ([CASLFORMULA], [CASLSign])
forall (m :: * -> *) a. Monad m => a -> m a
return ([CASLFORMULA]
els, [[CASLSign]] -> [CASLSign]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[CASLSign]]
s)

-- | Mapping of a list of pairs of descriptions
mapDescriptionListP :: Int -> [(ClassExpression, ClassExpression)]
                    -> Result ([(CASLFORMULA, CASLFORMULA)], [CASLSign])
mapDescriptionListP :: Int
-> [(ClassExpression, ClassExpression)]
-> Result ([(CASLFORMULA, CASLFORMULA)], [CASLSign])
mapDescriptionListP  n :: Int
n lst :: [(ClassExpression, ClassExpression)]
lst = do
    let (l :: [ClassExpression]
l, r :: [ClassExpression]
r) = [(ClassExpression, ClassExpression)]
-> ([ClassExpression], [ClassExpression])
forall a b. [(a, b)] -> ([a], [b])
unzip [(ClassExpression, ClassExpression)]
lst
    ([lls :: [CASLFORMULA]
lls, rls :: [CASLFORMULA]
rls], s :: [[CASLSign]]
s) <- ([ClassExpression] -> Result ([CASLFORMULA], [CASLSign]))
-> [[ClassExpression]] -> Result ([[CASLFORMULA]], [[CASLSign]])
forall (m :: * -> *) a b c.
Applicative m =>
(a -> m (b, c)) -> [a] -> m ([b], [c])
mapAndUnzipM (Int -> [ClassExpression] -> Result ([CASLFORMULA], [CASLSign])
mapDescriptionList Int
n) [[ClassExpression]
l, [ClassExpression]
r]
    ([(CASLFORMULA, CASLFORMULA)], [CASLSign])
-> Result ([(CASLFORMULA, CASLFORMULA)], [CASLSign])
forall (m :: * -> *) a. Monad m => a -> m a
return ([CASLFORMULA] -> [CASLFORMULA] -> [(CASLFORMULA, CASLFORMULA)]
forall t t1. [t] -> [t1] -> [(t, t1)]
zip [CASLFORMULA]
lls [CASLFORMULA]
rls, [[CASLSign]] -> [CASLSign]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[CASLSign]]
s)

mapCharact :: ObjectPropertyExpression -> Character
            -> Result CASLFORMULA
mapCharact :: ObjectPropertyExpression -> Character -> Result CASLFORMULA
mapCharact ope :: ObjectPropertyExpression
ope c :: Character
c = case Character
c of
    Functional -> do
        CASLFORMULA
so1 <- ObjectPropertyExpression -> Int -> Int -> Result CASLFORMULA
mapObjProp ObjectPropertyExpression
ope 1 2
        CASLFORMULA
so2 <- ObjectPropertyExpression -> Int -> Int -> Result CASLFORMULA
mapObjProp ObjectPropertyExpression
ope 1 3
        CASLFORMULA -> Result CASLFORMULA
forall (m :: * -> *) a. Monad m => a -> m a
return (CASLFORMULA -> Result CASLFORMULA)
-> CASLFORMULA -> Result CASLFORMULA
forall a b. (a -> b) -> a -> b
$ [Int] -> [CASLFORMULA] -> Int -> Int -> CASLFORMULA
forall f. [Int] -> [FORMULA f] -> Int -> Int -> FORMULA f
mkFIE [1, 2, 3] [CASLFORMULA
so1, CASLFORMULA
so2] 2 3
    InverseFunctional -> do
        CASLFORMULA
so1 <- ObjectPropertyExpression -> Int -> Int -> Result CASLFORMULA
mapObjProp ObjectPropertyExpression
ope 1 3
        CASLFORMULA
so2 <- ObjectPropertyExpression -> Int -> Int -> Result CASLFORMULA
mapObjProp ObjectPropertyExpression
ope 2 3
        CASLFORMULA -> Result CASLFORMULA
forall (m :: * -> *) a. Monad m => a -> m a
return (CASLFORMULA -> Result CASLFORMULA)
-> CASLFORMULA -> Result CASLFORMULA
forall a b. (a -> b) -> a -> b
$ [Int] -> [CASLFORMULA] -> Int -> Int -> CASLFORMULA
forall f. [Int] -> [FORMULA f] -> Int -> Int -> FORMULA f
mkFIE [1, 2, 3] [CASLFORMULA
so1, CASLFORMULA
so2] 1 2
    Reflexive -> do
        CASLFORMULA
so <- ObjectPropertyExpression -> Int -> Int -> Result CASLFORMULA
mapObjProp ObjectPropertyExpression
ope 1 1
        CASLFORMULA -> Result CASLFORMULA
forall (m :: * -> *) a. Monad m => a -> m a
return (CASLFORMULA -> Result CASLFORMULA)
-> CASLFORMULA -> Result CASLFORMULA
forall a b. (a -> b) -> a -> b
$ [Int] -> Int -> CASLFORMULA -> CASLFORMULA
forall f. [Int] -> Int -> FORMULA f -> FORMULA f
mkRI [1] 1 CASLFORMULA
so
    Irreflexive -> do
        CASLFORMULA
so <- ObjectPropertyExpression -> Int -> Int -> Result CASLFORMULA
mapObjProp ObjectPropertyExpression
ope 1 1
        CASLFORMULA -> Result CASLFORMULA
forall (m :: * -> *) a. Monad m => a -> m a
return (CASLFORMULA -> Result CASLFORMULA)
-> CASLFORMULA -> Result CASLFORMULA
forall a b. (a -> b) -> a -> b
$ [Int] -> Int -> CASLFORMULA -> CASLFORMULA
forall f. [Int] -> Int -> FORMULA f -> FORMULA f
mkRI [1] 1 (CASLFORMULA -> CASLFORMULA) -> CASLFORMULA -> CASLFORMULA
forall a b. (a -> b) -> a -> b
$ CASLFORMULA -> CASLFORMULA
forall f. FORMULA f -> FORMULA f
mkNeg CASLFORMULA
so
    Symmetric -> do
        CASLFORMULA
so1 <- ObjectPropertyExpression -> Int -> Int -> Result CASLFORMULA
mapObjProp ObjectPropertyExpression
ope 1 2
        CASLFORMULA
so2 <- ObjectPropertyExpression -> Int -> Int -> Result CASLFORMULA
mapObjProp ObjectPropertyExpression
ope 2 1
        CASLFORMULA -> Result CASLFORMULA
forall (m :: * -> *) a. Monad m => a -> m a
return (CASLFORMULA -> Result CASLFORMULA)
-> CASLFORMULA -> Result CASLFORMULA
forall a b. (a -> b) -> a -> b
$ [Int] -> CASLFORMULA -> CASLFORMULA
forall f. [Int] -> FORMULA f -> FORMULA f
mkVDecl [1, 2] (CASLFORMULA -> CASLFORMULA) -> CASLFORMULA -> CASLFORMULA
forall a b. (a -> b) -> a -> b
$ CASLFORMULA -> CASLFORMULA -> CASLFORMULA
forall f. FORMULA f -> FORMULA f -> FORMULA f
mkImpl CASLFORMULA
so1 CASLFORMULA
so2
    Asymmetric -> do
        CASLFORMULA
so1 <- ObjectPropertyExpression -> Int -> Int -> Result CASLFORMULA
mapObjProp ObjectPropertyExpression
ope 1 2
        CASLFORMULA
so2 <- ObjectPropertyExpression -> Int -> Int -> Result CASLFORMULA
mapObjProp ObjectPropertyExpression
ope 2 1
        CASLFORMULA -> Result CASLFORMULA
forall (m :: * -> *) a. Monad m => a -> m a
return (CASLFORMULA -> Result CASLFORMULA)
-> CASLFORMULA -> Result CASLFORMULA
forall a b. (a -> b) -> a -> b
$ [Int] -> CASLFORMULA -> CASLFORMULA
forall f. [Int] -> FORMULA f -> FORMULA f
mkVDecl [1, 2] (CASLFORMULA -> CASLFORMULA) -> CASLFORMULA -> CASLFORMULA
forall a b. (a -> b) -> a -> b
$ CASLFORMULA -> CASLFORMULA -> CASLFORMULA
forall f. FORMULA f -> FORMULA f -> FORMULA f
mkImpl CASLFORMULA
so1 (CASLFORMULA -> CASLFORMULA) -> CASLFORMULA -> CASLFORMULA
forall a b. (a -> b) -> a -> b
$ CASLFORMULA -> CASLFORMULA
forall f. FORMULA f -> FORMULA f
mkNeg CASLFORMULA
so2
    Antisymmetric -> do
        CASLFORMULA
so1 <- ObjectPropertyExpression -> Int -> Int -> Result CASLFORMULA
mapObjProp ObjectPropertyExpression
ope 1 2
        CASLFORMULA
so2 <- ObjectPropertyExpression -> Int -> Int -> Result CASLFORMULA
mapObjProp ObjectPropertyExpression
ope 2 1
        CASLFORMULA -> Result CASLFORMULA
forall (m :: * -> *) a. Monad m => a -> m a
return (CASLFORMULA -> Result CASLFORMULA)
-> CASLFORMULA -> Result CASLFORMULA
forall a b. (a -> b) -> a -> b
$ [Int] -> [CASLFORMULA] -> Int -> Int -> CASLFORMULA
forall f. [Int] -> [FORMULA f] -> Int -> Int -> FORMULA f
mkFIE [1, 2] [CASLFORMULA
so1, CASLFORMULA
so2] 1 2
    Transitive -> do
        CASLFORMULA
so1 <- ObjectPropertyExpression -> Int -> Int -> Result CASLFORMULA
mapObjProp ObjectPropertyExpression
ope 1 2
        CASLFORMULA
so2 <- ObjectPropertyExpression -> Int -> Int -> Result CASLFORMULA
mapObjProp ObjectPropertyExpression
ope 2 3
        CASLFORMULA
so3 <- ObjectPropertyExpression -> Int -> Int -> Result CASLFORMULA
mapObjProp ObjectPropertyExpression
ope 1 3
        CASLFORMULA -> Result CASLFORMULA
forall (m :: * -> *) a. Monad m => a -> m a
return (CASLFORMULA -> Result CASLFORMULA)
-> CASLFORMULA -> Result CASLFORMULA
forall a b. (a -> b) -> a -> b
$ [Int] -> CASLFORMULA -> CASLFORMULA
forall f. [Int] -> FORMULA f -> FORMULA f
mkVDecl [1, 2, 3] (CASLFORMULA -> CASLFORMULA) -> CASLFORMULA -> CASLFORMULA
forall a b. (a -> b) -> a -> b
$ [CASLFORMULA] -> CASLFORMULA -> CASLFORMULA
forall f. [FORMULA f] -> FORMULA f -> FORMULA f
implConj [CASLFORMULA
so1, CASLFORMULA
so2] CASLFORMULA
so3

-- | Mapping of ObjectSubPropertyChain
mapSubObjPropChain :: [ObjectPropertyExpression]
    -> ObjectPropertyExpression -> Result CASLFORMULA
mapSubObjPropChain :: [ObjectPropertyExpression]
-> ObjectPropertyExpression -> Result CASLFORMULA
mapSubObjPropChain props :: [ObjectPropertyExpression]
props oP :: ObjectPropertyExpression
oP = do
     let (_, vars :: [Int]
vars) = [(ObjectPropertyExpression, Int)]
-> ([ObjectPropertyExpression], [Int])
forall a b. [(a, b)] -> ([a], [b])
unzip ([(ObjectPropertyExpression, Int)]
 -> ([ObjectPropertyExpression], [Int]))
-> [(ObjectPropertyExpression, Int)]
-> ([ObjectPropertyExpression], [Int])
forall a b. (a -> b) -> a -> b
$ [ObjectPropertyExpression]
-> [Int] -> [(ObjectPropertyExpression, Int)]
forall t t1. [t] -> [t1] -> [(t, t1)]
zip (ObjectPropertyExpression
oPObjectPropertyExpression
-> [ObjectPropertyExpression] -> [ObjectPropertyExpression]
forall a. a -> [a] -> [a]
:[ObjectPropertyExpression]
props) [1 ..]
     -- because we need n+1 vars for a chain of n roles
     [CASLFORMULA]
oProps <- ((ObjectPropertyExpression, Int) -> Result CASLFORMULA)
-> [(ObjectPropertyExpression, Int)] -> Result [CASLFORMULA]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\ (z :: ObjectPropertyExpression
z, x :: Int
x) -> ObjectPropertyExpression -> Int -> Int -> Result CASLFORMULA
mapObjProp ObjectPropertyExpression
z Int
x (Int
xInt -> Int -> Int
forall a. Num a => a -> a -> a
+1)) ([(ObjectPropertyExpression, Int)] -> Result [CASLFORMULA])
-> [(ObjectPropertyExpression, Int)] -> Result [CASLFORMULA]
forall a b. (a -> b) -> a -> b
$
                 [ObjectPropertyExpression]
-> [Int] -> [(ObjectPropertyExpression, Int)]
forall t t1. [t] -> [t1] -> [(t, t1)]
zip [ObjectPropertyExpression]
props [Int]
vars
     CASLFORMULA
ooP <- ObjectPropertyExpression -> Int -> Int -> Result CASLFORMULA
mapObjProp ObjectPropertyExpression
oP 1 ([Int] -> Int
forall a. [a] -> a
head ([Int] -> Int) -> [Int] -> Int
forall a b. (a -> b) -> a -> b
$ [Int] -> [Int]
forall a. [a] -> [a]
reverse [Int]
vars)
     CASLFORMULA -> Result CASLFORMULA
forall (m :: * -> *) a. Monad m => a -> m a
return (CASLFORMULA -> Result CASLFORMULA)
-> CASLFORMULA -> Result CASLFORMULA
forall a b. (a -> b) -> a -> b
$ [Int] -> CASLFORMULA -> CASLFORMULA
forall f. [Int] -> FORMULA f -> FORMULA f
mkVDecl [Int]
vars (CASLFORMULA -> CASLFORMULA) -> CASLFORMULA -> CASLFORMULA
forall a b. (a -> b) -> a -> b
$ [CASLFORMULA] -> CASLFORMULA -> CASLFORMULA
forall f. [FORMULA f] -> FORMULA f -> FORMULA f
implConj [CASLFORMULA]
oProps CASLFORMULA
ooP

-- | Mapping of subobj properties
mapSubObjProp :: ObjectPropertyExpression
    -> ObjectPropertyExpression -> Int -> Result CASLFORMULA
mapSubObjProp :: ObjectPropertyExpression
-> ObjectPropertyExpression -> Int -> Result CASLFORMULA
mapSubObjProp e1 :: ObjectPropertyExpression
e1 e2 :: ObjectPropertyExpression
e2 a :: Int
a = do
    let b :: Int
b = Int
a Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1
    CASLFORMULA
l <- ObjectPropertyExpression -> Int -> Int -> Result CASLFORMULA
mapObjProp ObjectPropertyExpression
e1 Int
a Int
b
    CASLFORMULA
r <- ObjectPropertyExpression -> Int -> Int -> Result CASLFORMULA
mapObjProp ObjectPropertyExpression
e2 Int
a Int
b
    CASLFORMULA -> Result CASLFORMULA
forall (m :: * -> *) a. Monad m => a -> m a
return (CASLFORMULA -> Result CASLFORMULA)
-> CASLFORMULA -> Result CASLFORMULA
forall a b. (a -> b) -> a -> b
$ [VAR_DECL] -> CASLFORMULA -> Range -> CASLFORMULA
forall f. [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
mkForallRange ((Int -> VAR_DECL) -> [Int] -> [VAR_DECL]
forall a b. (a -> b) -> [a] -> [b]
map Int -> VAR_DECL
thingDecl [Int
a, Int
b]) (CASLFORMULA -> CASLFORMULA -> CASLFORMULA
forall f. FORMULA f -> FORMULA f -> FORMULA f
mkImpl CASLFORMULA
l CASLFORMULA
r) Range
nullRange

mkEDPairs :: [Int] -> Maybe AS.Relation -> [(FORMULA f, FORMULA f)]
    -> Result ([FORMULA f], [CASLSign])
mkEDPairs :: [Int]
-> Maybe Relation
-> [(FORMULA f, FORMULA f)]
-> Result ([FORMULA f], [CASLSign])
mkEDPairs il :: [Int]
il mr :: Maybe Relation
mr pairs :: [(FORMULA f, FORMULA f)]
pairs = do
    let ls :: [FORMULA f]
ls = ((FORMULA f, FORMULA f) -> FORMULA f)
-> [(FORMULA f, FORMULA f)] -> [FORMULA f]
forall a b. (a -> b) -> [a] -> [b]
map (\ (x :: FORMULA f
x, y :: FORMULA f
y) -> [Int] -> FORMULA f -> FORMULA f
forall f. [Int] -> FORMULA f -> FORMULA f
mkVDecl [Int]
il
            (FORMULA f -> FORMULA f) -> FORMULA f -> FORMULA f
forall a b. (a -> b) -> a -> b
$ case Relation -> Maybe Relation -> Relation
forall a. a -> Maybe a -> a
fromMaybe (String -> Relation
forall a. HasCallStack => String -> a
error "expected EDRelation") Maybe Relation
mr of
                EDRelation Equivalent -> FORMULA f -> FORMULA f -> FORMULA f
forall f. FORMULA f -> FORMULA f -> FORMULA f
mkEqv FORMULA f
x FORMULA f
y
                EDRelation Disjoint -> [FORMULA f] -> FORMULA f
forall f. [FORMULA f] -> FORMULA f
mkNC [FORMULA f
x, FORMULA f
y]
                _ -> String -> FORMULA f
forall a. HasCallStack => String -> a
error "expected EDRelation") [(FORMULA f, FORMULA f)]
pairs
    ([FORMULA f], [CASLSign]) -> Result ([FORMULA f], [CASLSign])
forall (m :: * -> *) a. Monad m => a -> m a
return ([FORMULA f]
ls, [])

mkEDPairs' :: [Int] -> Maybe AS.Relation -> [(FORMULA f, FORMULA f)]
    -> Result ([FORMULA f], [CASLSign])
mkEDPairs' :: [Int]
-> Maybe Relation
-> [(FORMULA f, FORMULA f)]
-> Result ([FORMULA f], [CASLSign])
mkEDPairs' [i1 :: Int
i1, i2 :: Int
i2] mr :: Maybe Relation
mr pairs :: [(FORMULA f, FORMULA f)]
pairs = do
    let ls :: [FORMULA f]
ls = ((FORMULA f, FORMULA f) -> FORMULA f)
-> [(FORMULA f, FORMULA f)] -> [FORMULA f]
forall a b. (a -> b) -> [a] -> [b]
map (\ (x :: FORMULA f
x, y :: FORMULA f
y) -> [Int] -> FORMULA f -> FORMULA f
forall f. [Int] -> FORMULA f -> FORMULA f
mkVDecl [Int
i1] (FORMULA f -> FORMULA f) -> FORMULA f -> FORMULA f
forall a b. (a -> b) -> a -> b
$ [Int] -> FORMULA f -> FORMULA f
forall f. [Int] -> FORMULA f -> FORMULA f
mkVDataDecl [Int
i2]
            (FORMULA f -> FORMULA f) -> FORMULA f -> FORMULA f
forall a b. (a -> b) -> a -> b
$ case Relation -> Maybe Relation -> Relation
forall a. a -> Maybe a -> a
fromMaybe (String -> Relation
forall a. HasCallStack => String -> a
error "expected EDRelation") Maybe Relation
mr of
                EDRelation Equivalent -> FORMULA f -> FORMULA f -> FORMULA f
forall f. FORMULA f -> FORMULA f -> FORMULA f
mkEqv FORMULA f
x FORMULA f
y
                EDRelation Disjoint -> [FORMULA f] -> FORMULA f
forall f. [FORMULA f] -> FORMULA f
mkNC [FORMULA f
x, FORMULA f
y]
                _ -> String -> FORMULA f
forall a. HasCallStack => String -> a
error "expected EDRelation") [(FORMULA f, FORMULA f)]
pairs
    ([FORMULA f], [CASLSign]) -> Result ([FORMULA f], [CASLSign])
forall (m :: * -> *) a. Monad m => a -> m a
return ([FORMULA f]
ls, [])
mkEDPairs' _ _ _ = String -> Result ([FORMULA f], [CASLSign])
forall a. HasCallStack => String -> a
error "wrong call of mkEDPairs'"

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

mapKey :: ClassExpression -> [FORMULA ()] -> [FORMULA ()]
    -> Int -> [Int] -> Int -> Result (FORMULA (), [CASLSign])
mapKey :: ClassExpression
-> [CASLFORMULA]
-> [CASLFORMULA]
-> Int
-> [Int]
-> Int
-> Result (CASLFORMULA, [CASLSign])
mapKey ce :: ClassExpression
ce pl :: [CASLFORMULA]
pl npl :: [CASLFORMULA]
npl p :: Int
p i :: [Int]
i h :: Int
h = do
    (nce :: CASLFORMULA
nce, s :: [CASLSign]
s) <- ClassExpression -> Int -> Result (CASLFORMULA, [CASLSign])
mapDescription ClassExpression
ce 1
    (c3 :: CASLFORMULA
c3, _) <- ClassExpression -> Int -> Result (CASLFORMULA, [CASLSign])
mapDescription ClassExpression
ce Int
p
    let un :: CASLFORMULA
un = [VAR_DECL] -> CASLFORMULA -> CASLFORMULA
forall f. [VAR_DECL] -> FORMULA f -> FORMULA f
mkForall [Int -> VAR_DECL
thingDecl Int
p] (CASLFORMULA -> CASLFORMULA) -> CASLFORMULA -> CASLFORMULA
forall a b. (a -> b) -> a -> b
$ [CASLFORMULA] -> CASLFORMULA -> CASLFORMULA
forall f. [FORMULA f] -> FORMULA f -> FORMULA f
implConj (CASLFORMULA
c3 CASLFORMULA -> [CASLFORMULA] -> [CASLFORMULA]
forall a. a -> [a] -> [a]
: [CASLFORMULA]
npl)
                (CASLFORMULA -> CASLFORMULA) -> CASLFORMULA -> CASLFORMULA
forall a b. (a -> b) -> a -> b
$ TERM () -> TERM () -> CASLFORMULA
forall f. TERM f -> TERM f -> FORMULA f
mkStEq (Int -> TERM ()
forall f. Int -> TERM f
qualThing Int
p) (TERM () -> CASLFORMULA) -> TERM () -> CASLFORMULA
forall a b. (a -> b) -> a -> b
$ Int -> TERM ()
forall f. Int -> TERM f
qualThing 1
    (CASLFORMULA, [CASLSign]) -> Result (CASLFORMULA, [CASLSign])
forall (m :: * -> *) a. Monad m => a -> m a
return ([VAR_DECL] -> CASLFORMULA -> CASLFORMULA
forall f. [VAR_DECL] -> FORMULA f -> FORMULA f
mkForall [Int -> VAR_DECL
thingDecl 1] (CASLFORMULA -> CASLFORMULA) -> CASLFORMULA -> CASLFORMULA
forall a b. (a -> b) -> a -> b
$ CASLFORMULA -> CASLFORMULA -> CASLFORMULA
forall f. FORMULA f -> FORMULA f -> FORMULA f
mkImpl CASLFORMULA
nce
            (CASLFORMULA -> CASLFORMULA) -> CASLFORMULA -> CASLFORMULA
forall a b. (a -> b) -> a -> b
$ [VAR_DECL] -> CASLFORMULA -> CASLFORMULA
forall f. [VAR_DECL] -> FORMULA f -> FORMULA f
mkExist (Int -> [Int] -> [VAR_DECL]
keyDecl Int
h [Int]
i) (CASLFORMULA -> CASLFORMULA) -> CASLFORMULA -> CASLFORMULA
forall a b. (a -> b) -> a -> b
$ [CASLFORMULA] -> CASLFORMULA
forall f. [FORMULA f] -> FORMULA f
conjunct ([CASLFORMULA] -> CASLFORMULA) -> [CASLFORMULA] -> CASLFORMULA
forall a b. (a -> b) -> a -> b
$ [CASLFORMULA]
pl [CASLFORMULA] -> [CASLFORMULA] -> [CASLFORMULA]
forall a. [a] -> [a] -> [a]
++ [CASLFORMULA
un], [CASLSign]
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 -> VAR_DECL
swrlVariableToVar iri :: IRI
iri = ((Token -> SORT -> VAR_DECL) -> SORT -> Token -> VAR_DECL
forall a b c. (a -> b -> c) -> b -> a -> c
flip Token -> SORT -> VAR_DECL
mkVarDecl) SORT
thing (Token -> VAR_DECL) -> Token -> VAR_DECL
forall a b. (a -> b) -> a -> b
$ 
    case String -> String -> Maybe String
forall a. Eq a => [a] -> [a] -> Maybe [a]
List.stripPrefix "urn:swrl#" (IRI -> String
showIRI IRI
iri) of
        Nothing -> SORT -> Token
idToSimpleId (SORT -> Token) -> (IRI -> SORT) -> IRI -> Token
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IRI -> SORT
uriToCaslId (IRI -> Token) -> IRI -> Token
forall a b. (a -> b) -> a -> b
$ IRI
iri
        Just var :: String
var -> String -> Token
genToken String
var

mapAxioms :: Axiom -> Result([CASLFORMULA], [CASLSign])
mapAxioms :: Axiom -> Result ([CASLFORMULA], [CASLSign])
mapAxioms axiom :: Axiom
axiom = case Axiom
axiom of
    Declaration _ _ -> ([CASLFORMULA], [CASLSign]) -> Result ([CASLFORMULA], [CASLSign])
forall (m :: * -> *) a. Monad m => a -> m a
return ([], [])

    ClassAxiom clAxiom :: ClassAxiom
clAxiom -> case ClassAxiom
clAxiom of
        SubClassOf _ sub :: ClassExpression
sub sup :: ClassExpression
sup -> do
            (domT :: CASLFORMULA
domT, s1 :: [CASLSign]
s1) <- ClassExpression -> Int -> Result (CASLFORMULA, [CASLSign])
mapDescription ClassExpression
sub 1
            (codT :: [CASLFORMULA]
codT, s2 :: [CASLSign]
s2) <- Int -> [ClassExpression] -> Result ([CASLFORMULA], [CASLSign])
mapDescriptionList 1 [ClassExpression
sup]
            ([CASLFORMULA], [CASLSign]) -> Result ([CASLFORMULA], [CASLSign])
forall (m :: * -> *) a. Monad m => a -> m a
return ((CASLFORMULA -> CASLFORMULA) -> [CASLFORMULA] -> [CASLFORMULA]
forall a b. (a -> b) -> [a] -> [b]
map (CASLFORMULA -> CASLFORMULA
forall f. FORMULA f -> FORMULA f
mk1VDecl (CASLFORMULA -> CASLFORMULA)
-> (CASLFORMULA -> CASLFORMULA) -> CASLFORMULA -> CASLFORMULA
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CASLFORMULA -> CASLFORMULA -> CASLFORMULA
forall f. FORMULA f -> FORMULA f -> FORMULA f
mkImpl CASLFORMULA
domT) [CASLFORMULA]
codT,
                    [CASLSign]
s1 [CASLSign] -> [CASLSign] -> [CASLSign]
forall a. [a] -> [a] -> [a]
++ [CASLSign]
s2)
    
        EquivalentClasses _ cel :: [ClassExpression]
cel -> do
            (els :: [(CASLFORMULA, CASLFORMULA)]
els, _) <- Int
-> [(ClassExpression, ClassExpression)]
-> Result ([(CASLFORMULA, CASLFORMULA)], [CASLSign])
mapDescriptionListP 1 ([(ClassExpression, ClassExpression)]
 -> Result ([(CASLFORMULA, CASLFORMULA)], [CASLSign]))
-> [(ClassExpression, ClassExpression)]
-> Result ([(CASLFORMULA, CASLFORMULA)], [CASLSign])
forall a b. (a -> b) -> a -> b
$ [ClassExpression]
-> [ClassExpression] -> [(ClassExpression, ClassExpression)]
forall t t1. [t] -> [t1] -> [(t, t1)]
comPairs [ClassExpression]
cel [ClassExpression]
cel
            [Int]
-> Maybe Relation
-> [(CASLFORMULA, CASLFORMULA)]
-> Result ([CASLFORMULA], [CASLSign])
forall f.
[Int]
-> Maybe Relation
-> [(FORMULA f, FORMULA f)]
-> Result ([FORMULA f], [CASLSign])
mkEDPairs [1] (Relation -> Maybe Relation
forall a. a -> Maybe a
Just (Relation -> Maybe Relation) -> Relation -> Maybe Relation
forall a b. (a -> b) -> a -> b
$ EquivOrDisjoint -> Relation
EDRelation EquivOrDisjoint
Equivalent) [(CASLFORMULA, CASLFORMULA)]
els

        DisjointClasses _ cel :: [ClassExpression]
cel -> do
            (els :: [(CASLFORMULA, CASLFORMULA)]
els, _) <- Int
-> [(ClassExpression, ClassExpression)]
-> Result ([(CASLFORMULA, CASLFORMULA)], [CASLSign])
mapDescriptionListP 1 ([(ClassExpression, ClassExpression)]
 -> Result ([(CASLFORMULA, CASLFORMULA)], [CASLSign]))
-> [(ClassExpression, ClassExpression)]
-> Result ([(CASLFORMULA, CASLFORMULA)], [CASLSign])
forall a b. (a -> b) -> a -> b
$ [ClassExpression]
-> [ClassExpression] -> [(ClassExpression, ClassExpression)]
forall t t1. [t] -> [t1] -> [(t, t1)]
comPairs [ClassExpression]
cel [ClassExpression]
cel
            [Int]
-> Maybe Relation
-> [(CASLFORMULA, CASLFORMULA)]
-> Result ([CASLFORMULA], [CASLSign])
forall f.
[Int]
-> Maybe Relation
-> [(FORMULA f, FORMULA f)]
-> Result ([FORMULA f], [CASLSign])
mkEDPairs [1] (Relation -> Maybe Relation
forall a. a -> Maybe a
Just (Relation -> Maybe Relation) -> Relation -> Maybe Relation
forall a b. (a -> b) -> a -> b
$ EquivOrDisjoint -> Relation
EDRelation EquivOrDisjoint
Disjoint) [(CASLFORMULA, CASLFORMULA)]
els

        DisjointUnion _ clIri :: IRI
clIri clsl :: [ClassExpression]
clsl -> do
            (decrs :: [CASLFORMULA]
decrs, s1 :: [CASLSign]
s1) <- Int -> [ClassExpression] -> Result ([CASLFORMULA], [CASLSign])
mapDescriptionList 1 [ClassExpression]
clsl
            (decrsS :: [(CASLFORMULA, CASLFORMULA)]
decrsS, s2 :: [CASLSign]
s2) <- Int
-> [(ClassExpression, ClassExpression)]
-> Result ([(CASLFORMULA, CASLFORMULA)], [CASLSign])
mapDescriptionListP 1 ([(ClassExpression, ClassExpression)]
 -> Result ([(CASLFORMULA, CASLFORMULA)], [CASLSign]))
-> [(ClassExpression, ClassExpression)]
-> Result ([(CASLFORMULA, CASLFORMULA)], [CASLSign])
forall a b. (a -> b) -> a -> b
$ [ClassExpression]
-> [ClassExpression] -> [(ClassExpression, ClassExpression)]
forall t t1. [t] -> [t1] -> [(t, t1)]
comPairs [ClassExpression]
clsl [ClassExpression]
clsl
            let decrsP :: [CASLFORMULA]
decrsP = ((CASLFORMULA, CASLFORMULA) -> CASLFORMULA)
-> [(CASLFORMULA, CASLFORMULA)] -> [CASLFORMULA]
forall a b. (a -> b) -> [a] -> [b]
map (\ (x :: CASLFORMULA
x, y :: CASLFORMULA
y) -> [CASLFORMULA] -> CASLFORMULA
forall f. [FORMULA f] -> FORMULA f
conjunct [CASLFORMULA
x, CASLFORMULA
y]) [(CASLFORMULA, CASLFORMULA)]
decrsS
            CASLFORMULA
mcls <- IRI -> Token -> Result CASLFORMULA
mapClassURI IRI
clIri (Token -> Result CASLFORMULA) -> Token -> Result CASLFORMULA
forall a b. (a -> b) -> a -> b
$ Int -> Token
mkNName 1
            ([CASLFORMULA], [CASLSign]) -> Result ([CASLFORMULA], [CASLSign])
forall (m :: * -> *) a. Monad m => a -> m a
return ([CASLFORMULA -> CASLFORMULA
forall f. FORMULA f -> FORMULA f
mk1VDecl (CASLFORMULA -> CASLFORMULA) -> CASLFORMULA -> CASLFORMULA
forall a b. (a -> b) -> a -> b
$ CASLFORMULA -> CASLFORMULA -> CASLFORMULA
forall f. FORMULA f -> FORMULA f -> FORMULA f
mkEqv CASLFORMULA
mcls (CASLFORMULA -> CASLFORMULA) -> CASLFORMULA -> CASLFORMULA
forall a b. (a -> b) -> a -> b
$ [CASLFORMULA] -> CASLFORMULA
forall f. [FORMULA f] -> FORMULA f
conjunct
                    [[CASLFORMULA] -> CASLFORMULA
forall f. [FORMULA f] -> FORMULA f
disjunct [CASLFORMULA]
decrs, [CASLFORMULA] -> CASLFORMULA
forall f. [FORMULA f] -> FORMULA f
mkNC [CASLFORMULA]
decrsP]], [CASLSign]
s1 [CASLSign] -> [CASLSign] -> [CASLSign]
forall a. [a] -> [a] -> [a]
++ [CASLSign]
s2)

    ObjectPropertyAxiom opAxiom :: ObjectPropertyAxiom
opAxiom -> case ObjectPropertyAxiom
opAxiom of
        SubObjectPropertyOf _ subOpExpr :: SubObjectPropertyExpression
subOpExpr supOpExpr :: ObjectPropertyExpression
supOpExpr -> case SubObjectPropertyExpression
subOpExpr of
            SubObjPropExpr_obj opExpr :: ObjectPropertyExpression
opExpr -> do
                [CASLFORMULA]
os <- ((ObjectPropertyExpression, ObjectPropertyExpression)
 -> Result CASLFORMULA)
-> [(ObjectPropertyExpression, ObjectPropertyExpression)]
-> Result [CASLFORMULA]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\ (o1 :: ObjectPropertyExpression
o1, o2 :: ObjectPropertyExpression
o2) -> ObjectPropertyExpression
-> ObjectPropertyExpression -> Int -> Result CASLFORMULA
mapSubObjProp ObjectPropertyExpression
o1 ObjectPropertyExpression
o2 3)
                    ([(ObjectPropertyExpression, ObjectPropertyExpression)]
 -> Result [CASLFORMULA])
-> [(ObjectPropertyExpression, ObjectPropertyExpression)]
-> Result [CASLFORMULA]
forall a b. (a -> b) -> a -> b
$ ObjectPropertyExpression
-> [ObjectPropertyExpression]
-> [(ObjectPropertyExpression, ObjectPropertyExpression)]
forall t s. t -> [s] -> [(t, s)]
mkPairs ObjectPropertyExpression
opExpr [ObjectPropertyExpression
supOpExpr]
                ([CASLFORMULA], [CASLSign]) -> Result ([CASLFORMULA], [CASLSign])
forall (m :: * -> *) a. Monad m => a -> m a
return ([CASLFORMULA]
os, [])
            SubObjPropExpr_exprchain opExprs :: [ObjectPropertyExpression]
opExprs -> do
                CASLFORMULA
os <- [ObjectPropertyExpression]
-> ObjectPropertyExpression -> Result CASLFORMULA
mapSubObjPropChain [ObjectPropertyExpression]
opExprs ObjectPropertyExpression
supOpExpr
                ([CASLFORMULA], [CASLSign]) -> Result ([CASLFORMULA], [CASLSign])
forall (m :: * -> *) a. Monad m => a -> m a
return ([CASLFORMULA
os], [])

        EquivalentObjectProperties _ opExprs :: [ObjectPropertyExpression]
opExprs -> do
            [(CASLFORMULA, CASLFORMULA)]
pairs <- Maybe ObjectPropertyExpression
-> [ObjectPropertyExpression]
-> Int
-> Int
-> Result [(CASLFORMULA, CASLFORMULA)]
mapComObjectPropsList Maybe ObjectPropertyExpression
forall a. Maybe a
Nothing [ObjectPropertyExpression]
opExprs 1 2
            [Int]
-> Maybe Relation
-> [(CASLFORMULA, CASLFORMULA)]
-> Result ([CASLFORMULA], [CASLSign])
forall f.
[Int]
-> Maybe Relation
-> [(FORMULA f, FORMULA f)]
-> Result ([FORMULA f], [CASLSign])
mkEDPairs [1, 2] (Relation -> Maybe Relation
forall a. a -> Maybe a
Just (Relation -> Maybe Relation) -> Relation -> Maybe Relation
forall a b. (a -> b) -> a -> b
$ EquivOrDisjoint -> Relation
EDRelation EquivOrDisjoint
Equivalent) [(CASLFORMULA, CASLFORMULA)]
pairs

        DisjointObjectProperties _ opExprs :: [ObjectPropertyExpression]
opExprs -> do
            [(CASLFORMULA, CASLFORMULA)]
pairs <- Maybe ObjectPropertyExpression
-> [ObjectPropertyExpression]
-> Int
-> Int
-> Result [(CASLFORMULA, CASLFORMULA)]
mapComObjectPropsList Maybe ObjectPropertyExpression
forall a. Maybe a
Nothing [ObjectPropertyExpression]
opExprs 1 2
            [Int]
-> Maybe Relation
-> [(CASLFORMULA, CASLFORMULA)]
-> Result ([CASLFORMULA], [CASLSign])
forall f.
[Int]
-> Maybe Relation
-> [(FORMULA f, FORMULA f)]
-> Result ([FORMULA f], [CASLSign])
mkEDPairs [1, 2] (Relation -> Maybe Relation
forall a. a -> Maybe a
Just (Relation -> Maybe Relation) -> Relation -> Maybe Relation
forall a b. (a -> b) -> a -> b
$ EquivOrDisjoint -> Relation
EDRelation EquivOrDisjoint
Disjoint) [(CASLFORMULA, CASLFORMULA)]
pairs

        InverseObjectProperties _ opExpr1 :: ObjectPropertyExpression
opExpr1 opExpr2 :: ObjectPropertyExpression
opExpr2 -> do
            [CASLFORMULA]
os1 <- (ObjectPropertyExpression -> Result CASLFORMULA)
-> [ObjectPropertyExpression] -> Result [CASLFORMULA]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\o1 :: ObjectPropertyExpression
o1 -> ObjectPropertyExpression -> Int -> Int -> Result CASLFORMULA
mapObjProp ObjectPropertyExpression
o1 1 2) [ObjectPropertyExpression
opExpr2]
            CASLFORMULA
o2 <- ObjectPropertyExpression -> Int -> Int -> Result CASLFORMULA
mapObjProp ObjectPropertyExpression
opExpr1 2 1
            ([CASLFORMULA], [CASLSign]) -> Result ([CASLFORMULA], [CASLSign])
forall (m :: * -> *) a. Monad m => a -> m a
return ((CASLFORMULA -> CASLFORMULA) -> [CASLFORMULA] -> [CASLFORMULA]
forall a b. (a -> b) -> [a] -> [b]
map ([Int] -> CASLFORMULA -> CASLFORMULA
forall f. [Int] -> FORMULA f -> FORMULA f
mkVDecl [1, 2] (CASLFORMULA -> CASLFORMULA)
-> (CASLFORMULA -> CASLFORMULA) -> CASLFORMULA -> CASLFORMULA
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CASLFORMULA -> CASLFORMULA -> CASLFORMULA
forall f. FORMULA f -> FORMULA f -> FORMULA f
mkEqv CASLFORMULA
o2) [CASLFORMULA]
os1, [])

        ObjectPropertyDomain _ opExpr :: ObjectPropertyExpression
opExpr clExpr :: ClassExpression
clExpr -> do
            CASLFORMULA
tobjP <- ObjectPropertyExpression -> Int -> Int -> Result CASLFORMULA
mapObjProp ObjectPropertyExpression
opExpr 1 2
            (tdsc :: [CASLFORMULA]
tdsc, s :: [[CASLSign]]
s) <- (ClassExpression -> Result (CASLFORMULA, [CASLSign]))
-> [ClassExpression] -> Result ([CASLFORMULA], [[CASLSign]])
forall (m :: * -> *) a b c.
Applicative m =>
(a -> m (b, c)) -> [a] -> m ([b], [c])
mapAndUnzipM (\c :: ClassExpression
c -> ClassExpression -> Int -> Result (CASLFORMULA, [CASLSign])
mapDescription ClassExpression
c 1) [ClassExpression
clExpr]
            let vars :: (Token, Token)
vars = (Int -> Token
mkNName 1, Int -> Token
mkNName 2)
            ([CASLFORMULA], [CASLSign]) -> Result ([CASLFORMULA], [CASLSign])
forall (m :: * -> *) a. Monad m => a -> m a
return ((CASLFORMULA -> CASLFORMULA) -> [CASLFORMULA] -> [CASLFORMULA]
forall a b. (a -> b) -> [a] -> [b]
map ([VAR_DECL]
-> [VAR_DECL] -> CASLFORMULA -> CASLFORMULA -> CASLFORMULA
forall f.
[VAR_DECL] -> [VAR_DECL] -> FORMULA f -> FORMULA f -> FORMULA f
mkFI [Token -> VAR_DECL
tokDecl (Token -> VAR_DECL) -> Token -> VAR_DECL
forall a b. (a -> b) -> a -> b
$ (Token, Token) -> Token
forall a b. (a, b) -> a
fst (Token, Token)
vars] [Token -> VAR_DECL
tokDecl (Token -> VAR_DECL) -> Token -> VAR_DECL
forall a b. (a -> b) -> a -> b
$ (Token, Token) -> Token
forall a b. (a, b) -> b
snd (Token, Token)
vars] CASLFORMULA
tobjP) [CASLFORMULA]
tdsc,
                    [[CASLSign]] -> [CASLSign]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[CASLSign]]
s)

        ObjectPropertyRange _ opExpr :: ObjectPropertyExpression
opExpr clExpr :: ClassExpression
clExpr -> do
            CASLFORMULA
tobjP <- ObjectPropertyExpression -> Int -> Int -> Result CASLFORMULA
mapObjProp ObjectPropertyExpression
opExpr 1 2
            (tdsc :: [CASLFORMULA]
tdsc, s :: [[CASLSign]]
s) <- (ClassExpression -> Result (CASLFORMULA, [CASLSign]))
-> [ClassExpression] -> Result ([CASLFORMULA], [[CASLSign]])
forall (m :: * -> *) a b c.
Applicative m =>
(a -> m (b, c)) -> [a] -> m ([b], [c])
mapAndUnzipM (\c :: ClassExpression
c -> ClassExpression -> Int -> Result (CASLFORMULA, [CASLSign])
mapDescription ClassExpression
c 2) [ClassExpression
clExpr]
            let vars :: (Token, Token)
vars = (Int -> Token
mkNName 2, Int -> Token
mkNName 1)
            ([CASLFORMULA], [CASLSign]) -> Result ([CASLFORMULA], [CASLSign])
forall (m :: * -> *) a. Monad m => a -> m a
return ((CASLFORMULA -> CASLFORMULA) -> [CASLFORMULA] -> [CASLFORMULA]
forall a b. (a -> b) -> [a] -> [b]
map ([VAR_DECL]
-> [VAR_DECL] -> CASLFORMULA -> CASLFORMULA -> CASLFORMULA
forall f.
[VAR_DECL] -> [VAR_DECL] -> FORMULA f -> FORMULA f -> FORMULA f
mkFI [Token -> VAR_DECL
tokDecl (Token -> VAR_DECL) -> Token -> VAR_DECL
forall a b. (a -> b) -> a -> b
$ (Token, Token) -> Token
forall a b. (a, b) -> a
fst (Token, Token)
vars] [Token -> VAR_DECL
tokDecl (Token -> VAR_DECL) -> Token -> VAR_DECL
forall a b. (a -> b) -> a -> b
$ (Token, Token) -> Token
forall a b. (a, b) -> b
snd (Token, Token)
vars] CASLFORMULA
tobjP) [CASLFORMULA]
tdsc,
                    [[CASLSign]] -> [CASLSign]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[CASLSign]]
s)

        FunctionalObjectProperty _ opExpr :: ObjectPropertyExpression
opExpr -> do
            [CASLFORMULA]
cl <- (Character -> Result CASLFORMULA)
-> [Character] -> Result [CASLFORMULA]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (ObjectPropertyExpression -> Character -> Result CASLFORMULA
mapCharact ObjectPropertyExpression
opExpr) [Character
Functional]
            ([CASLFORMULA], [CASLSign]) -> Result ([CASLFORMULA], [CASLSign])
forall (m :: * -> *) a. Monad m => a -> m a
return ([CASLFORMULA]
cl, [])

        InverseFunctionalObjectProperty _ opExpr :: ObjectPropertyExpression
opExpr -> do
            [CASLFORMULA]
cl <- (Character -> Result CASLFORMULA)
-> [Character] -> Result [CASLFORMULA]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (ObjectPropertyExpression -> Character -> Result CASLFORMULA
mapCharact ObjectPropertyExpression
opExpr) [Character
InverseFunctional]
            ([CASLFORMULA], [CASLSign]) -> Result ([CASLFORMULA], [CASLSign])
forall (m :: * -> *) a. Monad m => a -> m a
return ([CASLFORMULA]
cl, [])
            
        ReflexiveObjectProperty _ opExpr :: ObjectPropertyExpression
opExpr -> do
            [CASLFORMULA]
cl <- (Character -> Result CASLFORMULA)
-> [Character] -> Result [CASLFORMULA]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (ObjectPropertyExpression -> Character -> Result CASLFORMULA
mapCharact ObjectPropertyExpression
opExpr) [Character
Reflexive]
            ([CASLFORMULA], [CASLSign]) -> Result ([CASLFORMULA], [CASLSign])
forall (m :: * -> *) a. Monad m => a -> m a
return ([CASLFORMULA]
cl, [])

        IrreflexiveObjectProperty _ opExpr :: ObjectPropertyExpression
opExpr -> do
            [CASLFORMULA]
cl <- (Character -> Result CASLFORMULA)
-> [Character] -> Result [CASLFORMULA]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (ObjectPropertyExpression -> Character -> Result CASLFORMULA
mapCharact ObjectPropertyExpression
opExpr) [Character
Irreflexive]
            ([CASLFORMULA], [CASLSign]) -> Result ([CASLFORMULA], [CASLSign])
forall (m :: * -> *) a. Monad m => a -> m a
return ([CASLFORMULA]
cl, [])

        SymmetricObjectProperty _ opExpr :: ObjectPropertyExpression
opExpr -> do
            [CASLFORMULA]
cl <- (Character -> Result CASLFORMULA)
-> [Character] -> Result [CASLFORMULA]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (ObjectPropertyExpression -> Character -> Result CASLFORMULA
mapCharact ObjectPropertyExpression
opExpr) [Character
Symmetric]
            ([CASLFORMULA], [CASLSign]) -> Result ([CASLFORMULA], [CASLSign])
forall (m :: * -> *) a. Monad m => a -> m a
return ([CASLFORMULA]
cl, [])

        AsymmetricObjectProperty _ opExpr :: ObjectPropertyExpression
opExpr -> do
            [CASLFORMULA]
cl <- (Character -> Result CASLFORMULA)
-> [Character] -> Result [CASLFORMULA]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (ObjectPropertyExpression -> Character -> Result CASLFORMULA
mapCharact ObjectPropertyExpression
opExpr) [Character
Asymmetric]
            ([CASLFORMULA], [CASLSign]) -> Result ([CASLFORMULA], [CASLSign])
forall (m :: * -> *) a. Monad m => a -> m a
return ([CASLFORMULA]
cl, [])

        TransitiveObjectProperty _ opExpr :: ObjectPropertyExpression
opExpr -> do
            [CASLFORMULA]
cl <- (Character -> Result CASLFORMULA)
-> [Character] -> Result [CASLFORMULA]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (ObjectPropertyExpression -> Character -> Result CASLFORMULA
mapCharact ObjectPropertyExpression
opExpr) [Character
Transitive]
            ([CASLFORMULA], [CASLSign]) -> Result ([CASLFORMULA], [CASLSign])
forall (m :: * -> *) a. Monad m => a -> m a
return ([CASLFORMULA]
cl, [])

    DataPropertyAxiom dpAxiom :: DataPropertyAxiom
dpAxiom -> case DataPropertyAxiom
dpAxiom of
        SubDataPropertyOf _ subDpExpr :: IRI
subDpExpr supDpExpr :: IRI
supDpExpr -> do
            [CASLFORMULA]
os1 <- (IRI -> Result CASLFORMULA) -> [IRI] -> Result [CASLFORMULA]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\ o1 :: IRI
o1 -> IRI -> Int -> Int -> Result CASLFORMULA
mapDataProp IRI
o1 1 2) [IRI
supDpExpr]
            CASLFORMULA
o2 <- IRI -> Int -> Int -> Result CASLFORMULA
mapDataProp IRI
subDpExpr 1 2 -- was 2 1
            ([CASLFORMULA], [CASLSign]) -> Result ([CASLFORMULA], [CASLSign])
forall (m :: * -> *) a. Monad m => a -> m a
return ((CASLFORMULA -> CASLFORMULA) -> [CASLFORMULA] -> [CASLFORMULA]
forall a b. (a -> b) -> [a] -> [b]
map ([VAR_DECL] -> CASLFORMULA -> CASLFORMULA
forall f. [VAR_DECL] -> FORMULA f -> FORMULA f
mkForall [Int -> VAR_DECL
thingDecl 1, Int -> VAR_DECL
dataDecl 2]
                (CASLFORMULA -> CASLFORMULA)
-> (CASLFORMULA -> CASLFORMULA) -> CASLFORMULA -> CASLFORMULA
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CASLFORMULA -> CASLFORMULA -> CASLFORMULA
forall f. FORMULA f -> FORMULA f -> FORMULA f
mkImpl CASLFORMULA
o2) [CASLFORMULA]
os1, [])  
        
        EquivalentDataProperties _ dpExprs :: [IRI]
dpExprs -> do
            [(CASLFORMULA, CASLFORMULA)]
pairs <- Maybe IRI
-> [IRI] -> Int -> Int -> Result [(CASLFORMULA, CASLFORMULA)]
mapComDataPropsList Maybe IRI
forall a. Maybe a
Nothing [IRI]
dpExprs 1 2
            [Int]
-> Maybe Relation
-> [(CASLFORMULA, CASLFORMULA)]
-> Result ([CASLFORMULA], [CASLSign])
forall f.
[Int]
-> Maybe Relation
-> [(FORMULA f, FORMULA f)]
-> Result ([FORMULA f], [CASLSign])
mkEDPairs' [1, 2] (Relation -> Maybe Relation
forall a. a -> Maybe a
Just (Relation -> Maybe Relation) -> Relation -> Maybe Relation
forall a b. (a -> b) -> a -> b
$ EquivOrDisjoint -> Relation
EDRelation EquivOrDisjoint
Equivalent) [(CASLFORMULA, CASLFORMULA)]
pairs

        DisjointDataProperties _ dpExprs :: [IRI]
dpExprs -> do
            [(CASLFORMULA, CASLFORMULA)]
pairs <- Maybe IRI
-> [IRI] -> Int -> Int -> Result [(CASLFORMULA, CASLFORMULA)]
mapComDataPropsList Maybe IRI
forall a. Maybe a
Nothing [IRI]
dpExprs 1 2
            [Int]
-> Maybe Relation
-> [(CASLFORMULA, CASLFORMULA)]
-> Result ([CASLFORMULA], [CASLSign])
forall f.
[Int]
-> Maybe Relation
-> [(FORMULA f, FORMULA f)]
-> Result ([FORMULA f], [CASLSign])
mkEDPairs' [1, 2] (Relation -> Maybe Relation
forall a. a -> Maybe a
Just (Relation -> Maybe Relation) -> Relation -> Maybe Relation
forall a b. (a -> b) -> a -> b
$ EquivOrDisjoint -> Relation
EDRelation EquivOrDisjoint
Disjoint) [(CASLFORMULA, CASLFORMULA)]
pairs

        DataPropertyDomain _ dpExpr :: IRI
dpExpr clExpr :: ClassExpression
clExpr -> do
            (els :: [CASLFORMULA]
els, s :: [[CASLSign]]
s) <- (ClassExpression -> Result (CASLFORMULA, [CASLSign]))
-> [ClassExpression] -> Result ([CASLFORMULA], [[CASLSign]])
forall (m :: * -> *) a b c.
Applicative m =>
(a -> m (b, c)) -> [a] -> m ([b], [c])
mapAndUnzipM (\ c :: ClassExpression
c -> ClassExpression -> Int -> Result (CASLFORMULA, [CASLSign])
mapDescription ClassExpression
c 1) [ClassExpression
clExpr]
            CASLFORMULA
oEx <- IRI -> Int -> Int -> Result CASLFORMULA
mapDataProp IRI
dpExpr 1 2
            let vars :: (Token, Token)
vars = (Int -> Token
mkNName 1, Int -> Token
mkNName 2)
            ([CASLFORMULA], [CASLSign]) -> Result ([CASLFORMULA], [CASLSign])
forall (m :: * -> *) a. Monad m => a -> m a
return ((CASLFORMULA -> CASLFORMULA) -> [CASLFORMULA] -> [CASLFORMULA]
forall a b. (a -> b) -> [a] -> [b]
map ([VAR_DECL]
-> [VAR_DECL] -> CASLFORMULA -> CASLFORMULA -> CASLFORMULA
forall f.
[VAR_DECL] -> [VAR_DECL] -> FORMULA f -> FORMULA f -> FORMULA f
mkFI [Token -> VAR_DECL
tokDecl (Token -> VAR_DECL) -> Token -> VAR_DECL
forall a b. (a -> b) -> a -> b
$ (Token, Token) -> Token
forall a b. (a, b) -> a
fst (Token, Token)
vars]
                [Token -> SORT -> VAR_DECL
mkVarDecl ((Token, Token) -> Token
forall a b. (a, b) -> b
snd (Token, Token)
vars) SORT
dataS] CASLFORMULA
oEx) [CASLFORMULA]
els, [[CASLSign]] -> [CASLSign]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[CASLSign]]
s)

        DataPropertyRange _ dpExpr :: IRI
dpExpr dr :: DataRange
dr -> do
            CASLFORMULA
oEx <- IRI -> Int -> Int -> Result CASLFORMULA
mapDataProp IRI
dpExpr 1 2
            (odes :: [CASLFORMULA]
odes, s :: [[CASLSign]]
s) <- (DataRange -> Result (CASLFORMULA, [CASLSign]))
-> [DataRange] -> Result ([CASLFORMULA], [[CASLSign]])
forall (m :: * -> *) a b c.
Applicative m =>
(a -> m (b, c)) -> [a] -> m ([b], [c])
mapAndUnzipM (\r :: DataRange
r -> DataRange -> Int -> Result (CASLFORMULA, [CASLSign])
mapDataRange DataRange
r 2) [DataRange
dr]
            let vars :: (Token, Token)
vars = (Int -> Token
mkNName 1, Int -> Token
mkNName 2)
            ([CASLFORMULA], [CASLSign]) -> Result ([CASLFORMULA], [CASLSign])
forall (m :: * -> *) a. Monad m => a -> m a
return ((CASLFORMULA -> CASLFORMULA) -> [CASLFORMULA] -> [CASLFORMULA]
forall a b. (a -> b) -> [a] -> [b]
map ([VAR_DECL]
-> [VAR_DECL] -> CASLFORMULA -> CASLFORMULA -> CASLFORMULA
forall f.
[VAR_DECL] -> [VAR_DECL] -> FORMULA f -> FORMULA f -> FORMULA f
mkFEI [Token -> VAR_DECL
tokDecl (Token -> VAR_DECL) -> Token -> VAR_DECL
forall a b. (a -> b) -> a -> b
$ (Token, Token) -> Token
forall a b. (a, b) -> a
fst (Token, Token)
vars]
                        [Token -> VAR_DECL
tokDataDecl (Token -> VAR_DECL) -> Token -> VAR_DECL
forall a b. (a -> b) -> a -> b
$ (Token, Token) -> Token
forall a b. (a, b) -> b
snd (Token, Token)
vars] CASLFORMULA
oEx) [CASLFORMULA]
odes, [[CASLSign]] -> [CASLSign]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[CASLSign]]
s)

        FunctionalDataProperty _ dpExpr :: IRI
dpExpr -> do
            CASLFORMULA
so1 <- IRI -> Int -> Int -> Result CASLFORMULA
mapDataProp IRI
dpExpr 1 2
            CASLFORMULA
so2 <- IRI -> Int -> Int -> Result CASLFORMULA
mapDataProp IRI
dpExpr 1 3
            ([CASLFORMULA], [CASLSign]) -> Result ([CASLFORMULA], [CASLSign])
forall (m :: * -> *) a. Monad m => a -> m a
return ([[VAR_DECL] -> CASLFORMULA -> CASLFORMULA
forall f. [VAR_DECL] -> FORMULA f -> FORMULA f
mkForall (Int -> VAR_DECL
thingDecl 1 VAR_DECL -> [VAR_DECL] -> [VAR_DECL]
forall a. a -> [a] -> [a]
: (Int -> VAR_DECL) -> [Int] -> [VAR_DECL]
forall a b. (a -> b) -> [a] -> [b]
map Int -> VAR_DECL
dataDecl [2, 3]) (CASLFORMULA -> CASLFORMULA) -> CASLFORMULA -> CASLFORMULA
forall a b. (a -> b) -> a -> b
$ [CASLFORMULA] -> CASLFORMULA -> CASLFORMULA
forall f. [FORMULA f] -> FORMULA f -> FORMULA f
implConj
                        [CASLFORMULA
so1, CASLFORMULA
so2] (CASLFORMULA -> CASLFORMULA) -> CASLFORMULA -> CASLFORMULA
forall a b. (a -> b) -> a -> b
$ VAR_DECL -> TERM () -> CASLFORMULA
forall f. VAR_DECL -> TERM f -> FORMULA f
mkEqVar (Int -> VAR_DECL
dataDecl 2) (TERM () -> CASLFORMULA) -> TERM () -> CASLFORMULA
forall a b. (a -> b) -> a -> b
$ Int -> TERM ()
forall f. Int -> TERM f
qualData 3], [])

    DatatypeDefinition _ dt :: IRI
dt dr :: DataRange
dr -> do
        (odes :: CASLFORMULA
odes, s :: [CASLSign]
s) <- DataRange -> Int -> Result (CASLFORMULA, [CASLSign])
mapDataRange DataRange
dr 2
        ([CASLFORMULA], [CASLSign]) -> Result ([CASLFORMULA], [CASLSign])
forall (m :: * -> *) a. Monad m => a -> m a
return ([[Int] -> CASLFORMULA -> CASLFORMULA
forall f. [Int] -> FORMULA f -> FORMULA f
mkVDataDecl [2] (CASLFORMULA -> CASLFORMULA) -> CASLFORMULA -> CASLFORMULA
forall a b. (a -> b) -> a -> b
$ CASLFORMULA -> CASLFORMULA -> CASLFORMULA
forall f. FORMULA f -> FORMULA f -> FORMULA f
mkEqv CASLFORMULA
odes (CASLFORMULA -> CASLFORMULA) -> CASLFORMULA -> CASLFORMULA
forall a b. (a -> b) -> a -> b
$ TERM () -> SORT -> CASLFORMULA
forall f. TERM f -> SORT -> FORMULA f
mkMember
                (Int -> TERM ()
forall f. Int -> TERM f
qualData 2) (SORT -> CASLFORMULA) -> SORT -> CASLFORMULA
forall a b. (a -> b) -> a -> b
$ IRI -> SORT
uriToCaslId IRI
dt], [CASLSign]
s)

    
    HasKey _ ce :: ClassExpression
ce opl :: [ObjectPropertyExpression]
opl dpl :: [IRI]
dpl -> do
        let lo :: Int
lo = [ObjectPropertyExpression] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [ObjectPropertyExpression]
opl 
            ld :: Int
ld = [IRI] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [IRI]
dpl
            uptoOP :: [Int]
uptoOP = [2 .. Int
lo Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1]
            uptoDP :: [Int]
uptoDP = [Int
lo Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 2 .. Int
lo Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
ld Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1]
            tl :: Int
tl = Int
lo Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
ld Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 2
        [CASLFORMULA]
ol <- ((Int, ObjectPropertyExpression) -> Result CASLFORMULA)
-> [(Int, ObjectPropertyExpression)] -> Result [CASLFORMULA]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\ (n :: Int
n, o :: ObjectPropertyExpression
o) -> ObjectPropertyExpression -> Int -> Int -> Result CASLFORMULA
mapObjProp ObjectPropertyExpression
o 1 Int
n) ([(Int, ObjectPropertyExpression)] -> Result [CASLFORMULA])
-> [(Int, ObjectPropertyExpression)] -> Result [CASLFORMULA]
forall a b. (a -> b) -> a -> b
$ [Int]
-> [ObjectPropertyExpression] -> [(Int, ObjectPropertyExpression)]
forall t t1. [t] -> [t1] -> [(t, t1)]
zip [Int]
uptoOP [ObjectPropertyExpression]
opl
        [CASLFORMULA]
nol <- ((Int, ObjectPropertyExpression) -> Result CASLFORMULA)
-> [(Int, ObjectPropertyExpression)] -> Result [CASLFORMULA]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\ (n :: Int
n, o :: ObjectPropertyExpression
o) -> ObjectPropertyExpression -> Int -> Int -> Result CASLFORMULA
mapObjProp ObjectPropertyExpression
o Int
tl Int
n) ([(Int, ObjectPropertyExpression)] -> Result [CASLFORMULA])
-> [(Int, ObjectPropertyExpression)] -> Result [CASLFORMULA]
forall a b. (a -> b) -> a -> b
$ [Int]
-> [ObjectPropertyExpression] -> [(Int, ObjectPropertyExpression)]
forall t t1. [t] -> [t1] -> [(t, t1)]
zip [Int]
uptoOP [ObjectPropertyExpression]
opl
        [CASLFORMULA]
dl <- ((Int, IRI) -> Result CASLFORMULA)
-> [(Int, IRI)] -> Result [CASLFORMULA]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\ (n :: Int
n, d :: IRI
d) -> IRI -> Int -> Int -> Result CASLFORMULA
mapDataProp IRI
d 1 Int
n) ([(Int, IRI)] -> Result [CASLFORMULA])
-> [(Int, IRI)] -> Result [CASLFORMULA]
forall a b. (a -> b) -> a -> b
$ [Int] -> [IRI] -> [(Int, IRI)]
forall t t1. [t] -> [t1] -> [(t, t1)]
zip [Int]
uptoDP [IRI]
dpl
        [CASLFORMULA]
ndl <- ((Int, IRI) -> Result CASLFORMULA)
-> [(Int, IRI)] -> Result [CASLFORMULA]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\ (n :: Int
n, d :: IRI
d) -> IRI -> Int -> Int -> Result CASLFORMULA
mapDataProp IRI
d Int
tl Int
n) ([(Int, IRI)] -> Result [CASLFORMULA])
-> [(Int, IRI)] -> Result [CASLFORMULA]
forall a b. (a -> b) -> a -> b
$ [Int] -> [IRI] -> [(Int, IRI)]
forall t t1. [t] -> [t1] -> [(t, t1)]
zip [Int]
uptoDP [IRI]
dpl
        (keys :: CASLFORMULA
keys, s :: [CASLSign]
s) <-
            ClassExpression
-> [CASLFORMULA]
-> [CASLFORMULA]
-> Int
-> [Int]
-> Int
-> Result (CASLFORMULA, [CASLSign])
mapKey ClassExpression
ce ([CASLFORMULA]
ol [CASLFORMULA] -> [CASLFORMULA] -> [CASLFORMULA]
forall a. [a] -> [a] -> [a]
++ [CASLFORMULA]
dl) ([CASLFORMULA]
nol [CASLFORMULA] -> [CASLFORMULA] -> [CASLFORMULA]
forall a. [a] -> [a] -> [a]
++ [CASLFORMULA]
ndl) Int
tl ([Int]
uptoOP [Int] -> [Int] -> [Int]
forall a. [a] -> [a] -> [a]
++ [Int]
uptoDP) Int
lo
        ([CASLFORMULA], [CASLSign]) -> Result ([CASLFORMULA], [CASLSign])
forall (m :: * -> *) a. Monad m => a -> m a
return ([CASLFORMULA
keys], [CASLSign]
s)

    Assertion assertion :: Assertion
assertion -> case Assertion
assertion of
        SameIndividual _ inds :: [IRI]
inds -> do
            let (mi :: Maybe IRI
mi, rest :: [IRI]
rest) = case [IRI]
inds of
                    (iri :: IRI
iri:r :: [IRI]
r) -> (IRI -> Maybe IRI
forall a. a -> Maybe a
Just IRI
iri, [IRI]
r)
                    _ -> (Maybe IRI
forall a. Maybe a
Nothing, [IRI]
inds)
            [CASLFORMULA]
fs <- SameOrDifferent -> Maybe IRI -> [IRI] -> Result [CASLFORMULA]
mapComIndivList SameOrDifferent
Same Maybe IRI
mi [IRI]
rest
            ([CASLFORMULA], [CASLSign]) -> Result ([CASLFORMULA], [CASLSign])
forall (m :: * -> *) a. Monad m => a -> m a
return ([CASLFORMULA]
fs, [])

        DifferentIndividuals _ inds :: [IRI]
inds -> do
            let (mi :: Maybe IRI
mi, rest :: [IRI]
rest) = case [IRI]
inds of
                    (iri :: IRI
iri:r :: [IRI]
r) -> (IRI -> Maybe IRI
forall a. a -> Maybe a
Just IRI
iri, [IRI]
r)
                    _ -> (Maybe IRI
forall a. Maybe a
Nothing, [IRI]
inds)
            [CASLFORMULA]
fs <- SameOrDifferent -> Maybe IRI -> [IRI] -> Result [CASLFORMULA]
mapComIndivList SameOrDifferent
Different Maybe IRI
mi [IRI]
rest
            ([CASLFORMULA], [CASLSign]) -> Result ([CASLFORMULA], [CASLSign])
forall (m :: * -> *) a. Monad m => a -> m a
return ([CASLFORMULA]
fs, [])

        ClassAssertion _ ce :: ClassExpression
ce iIri :: IRI
iIri -> do
            (els :: [CASLFORMULA]
els, s :: [[CASLSign]]
s) <- (ClassExpression -> Result (CASLFORMULA, [CASLSign]))
-> [ClassExpression] -> Result ([CASLFORMULA], [[CASLSign]])
forall (m :: * -> *) a b c.
Applicative m =>
(a -> m (b, c)) -> [a] -> m ([b], [c])
mapAndUnzipM (\c :: ClassExpression
c -> ClassExpression -> Int -> Result (CASLFORMULA, [CASLSign])
mapDescription ClassExpression
c 1) [ClassExpression
ce]
            TERM ()
inD <- IRI -> Result (TERM ())
mapIndivURI IRI
iIri
            let els' :: [CASLFORMULA]
els' = (CASLFORMULA -> CASLFORMULA) -> [CASLFORMULA] -> [CASLFORMULA]
forall a b. (a -> b) -> [a] -> [b]
map (Token -> SORT -> TERM () -> CASLFORMULA -> CASLFORMULA
forall f.
FormExtension f =>
Token -> SORT -> TERM f -> FORMULA f -> FORMULA f
substitute (Int -> Token
mkNName 1) SORT
thing TERM ()
inD) [CASLFORMULA]
els
            ([CASLFORMULA], [CASLSign]) -> Result ([CASLFORMULA], [CASLSign])
forall (m :: * -> *) a. Monad m => a -> m a
return ( [CASLFORMULA]
els', [[CASLSign]] -> [CASLSign]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[CASLSign]]
s)

        ObjectPropertyAssertion _ op :: ObjectPropertyExpression
op si :: IRI
si ti :: IRI
ti -> do
            CASLFORMULA
oPropH <- ObjectPropertyExpression
-> VarOrIndi -> VarOrIndi -> Result CASLFORMULA
mapObjPropI ObjectPropertyExpression
op (IRI -> VarOrIndi
OIndi IRI
si) (IRI -> VarOrIndi
OIndi IRI
ti)
            ([CASLFORMULA], [CASLSign]) -> Result ([CASLFORMULA], [CASLSign])
forall (m :: * -> *) a. Monad m => a -> m a
return ([CASLFORMULA
oPropH], [])

        NegativeObjectPropertyAssertion _ op :: ObjectPropertyExpression
op si :: IRI
si ti :: IRI
ti -> do
            CASLFORMULA
oPropH <- ObjectPropertyExpression
-> VarOrIndi -> VarOrIndi -> Result CASLFORMULA
mapObjPropI ObjectPropertyExpression
op (IRI -> VarOrIndi
OIndi IRI
si) (IRI -> VarOrIndi
OIndi IRI
ti)
            let oProp :: CASLFORMULA
oProp = CASLFORMULA -> Range -> CASLFORMULA
forall f. FORMULA f -> Range -> FORMULA f
Negation CASLFORMULA
oPropH Range
nullRange
            ([CASLFORMULA], [CASLSign]) -> Result ([CASLFORMULA], [CASLSign])
forall (m :: * -> *) a. Monad m => a -> m a
return ([CASLFORMULA
oProp], [])

        DataPropertyAssertion _ dp :: IRI
dp si :: IRI
si tv :: Literal
tv -> do
            TERM ()
inS <- IRI -> Result (TERM ())
mapIndivURI IRI
si
            TERM ()
inT <- Literal -> Result (TERM ())
mapLiteral Literal
tv
            CASLFORMULA
oProp <- IRI -> Int -> Int -> Result CASLFORMULA
mapDataProp IRI
dp 1 2
            ([CASLFORMULA], [CASLSign]) -> Result ([CASLFORMULA], [CASLSign])
forall (m :: * -> *) a. Monad m => a -> m a
return ([[VAR_DECL] -> CASLFORMULA -> CASLFORMULA
forall f. [VAR_DECL] -> FORMULA f -> FORMULA f
mkForall [Int -> VAR_DECL
thingDecl 1, Int -> VAR_DECL
dataDecl 2] (CASLFORMULA -> CASLFORMULA) -> CASLFORMULA -> CASLFORMULA
forall a b. (a -> b) -> a -> b
$ [CASLFORMULA] -> CASLFORMULA -> CASLFORMULA
forall f. [FORMULA f] -> FORMULA f -> FORMULA f
implConj
                [Int -> TERM () -> CASLFORMULA
forall f. Int -> TERM f -> FORMULA f
mkEqDecl 1 TERM ()
inS, VAR_DECL -> TERM () -> CASLFORMULA
forall f. VAR_DECL -> TERM f -> FORMULA f
mkEqVar (Int -> VAR_DECL
dataDecl 2) (TERM () -> CASLFORMULA) -> TERM () -> CASLFORMULA
forall a b. (a -> b) -> a -> b
$ TERM () -> SORT -> TERM ()
upcast TERM ()
inT SORT
dataS] CASLFORMULA
oProp],
                [])

        NegativeDataPropertyAssertion _ dp :: IRI
dp si :: IRI
si tv :: Literal
tv -> do
            TERM ()
inS <- IRI -> Result (TERM ())
mapIndivURI IRI
si
            TERM ()
inT <- Literal -> Result (TERM ())
mapLiteral Literal
tv
            CASLFORMULA
oPropH <- IRI -> Int -> Int -> Result CASLFORMULA
mapDataProp IRI
dp 1 2
            let oProp :: CASLFORMULA
oProp = CASLFORMULA -> Range -> CASLFORMULA
forall f. FORMULA f -> Range -> FORMULA f
Negation CASLFORMULA
oPropH Range
nullRange
            ([CASLFORMULA], [CASLSign]) -> Result ([CASLFORMULA], [CASLSign])
forall (m :: * -> *) a. Monad m => a -> m a
return ([[VAR_DECL] -> CASLFORMULA -> CASLFORMULA
forall f. [VAR_DECL] -> FORMULA f -> FORMULA f
mkForall [Int -> VAR_DECL
thingDecl 1, Int -> VAR_DECL
dataDecl 2] (CASLFORMULA -> CASLFORMULA) -> CASLFORMULA -> CASLFORMULA
forall a b. (a -> b) -> a -> b
$ [CASLFORMULA] -> CASLFORMULA -> CASLFORMULA
forall f. [FORMULA f] -> FORMULA f -> FORMULA f
implConj
                [Int -> TERM () -> CASLFORMULA
forall f. Int -> TERM f -> FORMULA f
mkEqDecl 1 TERM ()
inS, VAR_DECL -> TERM () -> CASLFORMULA
forall f. VAR_DECL -> TERM f -> FORMULA f
mkEqVar (Int -> VAR_DECL
dataDecl 2) (TERM () -> CASLFORMULA) -> TERM () -> CASLFORMULA
forall a b. (a -> b) -> a -> b
$ TERM () -> SORT -> TERM ()
upcast TERM ()
inT SORT
dataS] CASLFORMULA
oProp],
                [])

    AnnotationAxiom _ -> ([CASLFORMULA], [CASLSign]) -> Result ([CASLFORMULA], [CASLSign])
forall (m :: * -> *) a. Monad m => a -> m a
return ([], [])

    Rule rule :: Rule
rule -> case Rule
rule of
        DLSafeRule _ b :: Body
b h :: Body
h ->
            let vars :: [IRI]
vars = Set IRI -> [IRI]
forall a. Set a -> [a]
Set.toList (Set IRI -> [IRI]) -> ([Set IRI] -> Set IRI) -> [Set IRI] -> [IRI]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Set IRI] -> Set IRI
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions ([Set IRI] -> [IRI]) -> [Set IRI] -> [IRI]
forall a b. (a -> b) -> a -> b
$ Atom -> Set IRI
getVariablesFromAtom (Atom -> Set IRI) -> Body -> [Set IRI]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Body
b Body -> Body -> Body
forall a. [a] -> [a] -> [a]
++ Body
h)
                names :: [VAR_DECL]
names = IRI -> VAR_DECL
swrlVariableToVar (IRI -> VAR_DECL) -> [IRI] -> [VAR_DECL]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [IRI]
vars
                f :: ([CASLFORMULA], [CASLSign], Int)
-> Atom -> Result ([CASLFORMULA], [CASLSign], Int)
f (s :: [CASLFORMULA]
s, sig :: [CASLSign]
sig, startVal :: Int
startVal) at :: Atom
at = do
                    (sentences' :: [CASLFORMULA]
sentences', sig' :: [CASLSign]
sig', offsetValue :: Int
offsetValue) <- Int -> Atom -> Result ([CASLFORMULA], [CASLSign], Int)
atomToSentence Int
startVal Atom
at
                    ([CASLFORMULA], [CASLSign], Int)
-> Result ([CASLFORMULA], [CASLSign], Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ([CASLFORMULA]
s [CASLFORMULA] -> [CASLFORMULA] -> [CASLFORMULA]
forall a. [a] -> [a] -> [a]
++ [CASLFORMULA]
sentences', [CASLSign]
sig [CASLSign] -> [CASLSign] -> [CASLSign]
forall a. [a] -> [a] -> [a]
++ [CASLSign]
sig', Int
offsetValue)

                g :: Int -> t Atom -> Result ([CASLFORMULA], [CASLSign], Int)
g startVal :: Int
startVal atoms :: t Atom
atoms = (([CASLFORMULA], [CASLSign], Int)
 -> Atom -> Result ([CASLFORMULA], [CASLSign], Int))
-> ([CASLFORMULA], [CASLSign], Int)
-> t Atom
-> Result ([CASLFORMULA], [CASLSign], Int)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM ([CASLFORMULA], [CASLSign], Int)
-> Atom -> Result ([CASLFORMULA], [CASLSign], Int)
f ([], [], Int
startVal) t Atom
atoms
            in do
                (antecedentSen :: [CASLFORMULA]
antecedentSen, sig1 :: [CASLSign]
sig1, offsetValue :: Int
offsetValue) <- Int -> Body -> Result ([CASLFORMULA], [CASLSign], Int)
forall (t :: * -> *).
Foldable t =>
Int -> t Atom -> Result ([CASLFORMULA], [CASLSign], Int)
g 1 Body
b
                let antecedent :: CASLFORMULA
antecedent = [CASLFORMULA] -> CASLFORMULA
forall f. [FORMULA f] -> FORMULA f
conjunct [CASLFORMULA]
antecedentSen
                
                (consequentSen :: [CASLFORMULA]
consequentSen, sig2 :: [CASLSign]
sig2, lastVar :: Int
lastVar) <- Int -> Body -> Result ([CASLFORMULA], [CASLSign], Int)
forall (t :: * -> *).
Foldable t =>
Int -> t Atom -> Result ([CASLFORMULA], [CASLSign], Int)
g Int
offsetValue Body
h
                let consequent :: CASLFORMULA
consequent = [CASLFORMULA] -> CASLFORMULA
forall f. [FORMULA f] -> FORMULA f
conjunct [CASLFORMULA]
consequentSen

                
                let impl :: CASLFORMULA
impl = CASLFORMULA -> CASLFORMULA -> CASLFORMULA
forall f. FORMULA f -> FORMULA f -> FORMULA f
mkImpl CASLFORMULA
antecedent CASLFORMULA
consequent
                ([CASLFORMULA], [CASLSign]) -> Result ([CASLFORMULA], [CASLSign])
forall (m :: * -> *) a. Monad m => a -> m a
return (([CASLFORMULA], [CASLSign]) -> Result ([CASLFORMULA], [CASLSign]))
-> ([CASLFORMULA], [CASLSign])
-> Result ([CASLFORMULA], [CASLSign])
forall a b. (a -> b) -> a -> b
$ ([[VAR_DECL] -> CASLFORMULA -> CASLFORMULA
forall f. [VAR_DECL] -> FORMULA f -> FORMULA f
mkForall ([VAR_DECL]
names [VAR_DECL] -> [VAR_DECL] -> [VAR_DECL]
forall a. [a] -> [a] -> [a]
++ (Int -> VAR_DECL) -> [Int] -> [VAR_DECL]
forall a b. (a -> b) -> [a] -> [b]
map Int -> VAR_DECL
thingDecl [1..Int
lastVar Int -> Int -> Int
forall a. Num a => a -> a -> a
- 1]) CASLFORMULA
impl], [CASLSign]
sig1 [CASLSign] -> [CASLSign] -> [CASLSign]
forall a. [a] -> [a] -> [a]
++ [CASLSign]
sig2)
        DGRule _ _ _ -> String -> Result ([CASLFORMULA], [CASLSign])
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail "Translating DGRules is not supported yet!"
    DGAxiom _ _ _ _ _ -> String -> Result ([CASLFORMULA], [CASLSign])
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail "Translating DGAxioms is not supported yet!"


iArgToTerm :: IndividualArg -> Result(TERM ())
iArgToTerm :: IndividualArg -> Result (TERM ())
iArgToTerm arg :: IndividualArg
arg = case IndividualArg
arg of
    IVar v :: IRI
v -> TERM () -> Result (TERM ())
forall (m :: * -> *) a. Monad m => a -> m a
return (TERM () -> Result (TERM ()))
-> (IRI -> TERM ()) -> IRI -> Result (TERM ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VAR_DECL -> TERM ()
forall f. VAR_DECL -> TERM f
toQualVar (VAR_DECL -> TERM ()) -> (IRI -> VAR_DECL) -> IRI -> TERM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IRI -> VAR_DECL
swrlVariableToVar (IRI -> Result (TERM ())) -> IRI -> Result (TERM ())
forall a b. (a -> b) -> a -> b
$ IRI
v
    IArg iri :: IRI
iri -> IRI -> Result (TERM ())
mapIndivURI IRI
iri

iArgToVarOrIndi :: IndividualArg -> VarOrIndi
iArgToVarOrIndi :: IndividualArg -> VarOrIndi
iArgToVarOrIndi arg :: IndividualArg
arg = case IndividualArg
arg of
    IVar v :: IRI
v -> IRI -> VarOrIndi
OIndi IRI
v
    IArg iri :: IRI
iri -> IRI -> VarOrIndi
OIndi IRI
iri


iArgToIRI :: IndividualArg -> IRI
iArgToIRI :: IndividualArg -> IRI
iArgToIRI arg :: IndividualArg
arg = case IndividualArg
arg of
    IVar var :: IRI
var -> IRI
var
    IArg ind :: IRI
ind -> IRI
ind


dArgToTerm :: DataArg -> Result (TERM ())
dArgToTerm :: DataArg -> Result (TERM ())
dArgToTerm arg :: DataArg
arg = case DataArg
arg of
    DVar var :: IRI
var -> TERM () -> Result (TERM ())
forall (m :: * -> *) a. Monad m => a -> m a
return (TERM () -> Result (TERM ()))
-> (IRI -> TERM ()) -> IRI -> Result (TERM ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VAR_DECL -> TERM ()
forall f. VAR_DECL -> TERM f
toQualVar (VAR_DECL -> TERM ()) -> (IRI -> VAR_DECL) -> IRI -> TERM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
.  Token -> VAR_DECL
tokDataDecl (Token -> VAR_DECL) -> (IRI -> Token) -> IRI -> VAR_DECL
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IRI -> Token
uriToTok (IRI -> Result (TERM ())) -> IRI -> Result (TERM ())
forall a b. (a -> b) -> a -> b
$ IRI
var
    DArg lit :: Literal
lit -> Literal -> Result (TERM ())
mapLiteral Literal
lit

atomToSentence :: Int -> Atom -> Result ([CASLFORMULA], [CASLSign], Int)
atomToSentence :: Int -> Atom -> Result ([CASLFORMULA], [CASLSign], Int)
atomToSentence startVar :: Int
startVar atom :: Atom
atom = case Atom
atom of
    ClassAtom clExpr :: ClassExpression
clExpr iarg :: IndividualArg
iarg -> do 
        (el :: CASLFORMULA
el, sigs :: [CASLSign]
sigs) <- ClassExpression -> Int -> Result (CASLFORMULA, [CASLSign])
mapDescription ClassExpression
clExpr Int
startVar
        TERM ()
inD <- IndividualArg -> Result (TERM ())
iArgToTerm IndividualArg
iarg
        let el' :: CASLFORMULA
el' = Token -> SORT -> TERM () -> CASLFORMULA -> CASLFORMULA
forall f.
FormExtension f =>
Token -> SORT -> TERM f -> FORMULA f -> FORMULA f
substitute (Int -> Token
mkNName Int
startVar) SORT
thing TERM ()
inD CASLFORMULA
el
        ([CASLFORMULA], [CASLSign], Int)
-> Result ([CASLFORMULA], [CASLSign], Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ([CASLFORMULA
el'], [CASLSign]
sigs, Int
startVar)
        
    DataRangeAtom dr :: DataRange
dr darg :: DataArg
darg -> do
        TERM ()
dt <- DataArg -> Result (TERM ())
dArgToTerm DataArg
darg
        (odes :: CASLFORMULA
odes, s :: [CASLSign]
s) <- DataRange -> TERM () -> Result (CASLFORMULA, [CASLSign])
mapDataRangeAux DataRange
dr TERM ()
dt
        ([CASLFORMULA], [CASLSign], Int)
-> Result ([CASLFORMULA], [CASLSign], Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ([Token -> SORT -> TERM () -> CASLFORMULA -> CASLFORMULA
forall f.
FormExtension f =>
Token -> SORT -> TERM f -> FORMULA f -> FORMULA f
substitute (Int -> Token
mkNName 1) SORT
thing TERM ()
dt CASLFORMULA
odes], [CASLSign]
s, Int
startVar)

    ObjectPropertyAtom opExpr :: ObjectPropertyExpression
opExpr iarg1 :: IndividualArg
iarg1 iarg2 :: IndividualArg
iarg2 -> do
        let si :: VarOrIndi
si = IndividualArg -> VarOrIndi
iArgToVarOrIndi IndividualArg
iarg1
            ti :: VarOrIndi
ti = IndividualArg -> VarOrIndi
iArgToVarOrIndi IndividualArg
iarg2
        CASLFORMULA
oPropH <- ObjectPropertyExpression
-> VarOrIndi -> VarOrIndi -> Result CASLFORMULA
mapObjPropI ObjectPropertyExpression
opExpr VarOrIndi
si VarOrIndi
ti
        ([CASLFORMULA], [CASLSign], Int)
-> Result ([CASLFORMULA], [CASLSign], Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ([CASLFORMULA
oPropH], [], Int
startVar)

    DataPropertyAtom dpExpr :: IRI
dpExpr iarg :: IndividualArg
iarg darg :: DataArg
darg -> do
        let a :: Int
a = 1
            b :: Int
b = 2
        TERM ()
inS <- IndividualArg -> Result (TERM ())
iArgToTerm IndividualArg
iarg
        TERM ()
inT <- DataArg -> Result (TERM ())
dArgToTerm DataArg
darg
        CASLFORMULA
oProp <- IRI -> Int -> Int -> Result CASLFORMULA
mapDataProp IRI
dpExpr Int
a Int
b
        ([CASLFORMULA], [CASLSign], Int)
-> Result ([CASLFORMULA], [CASLSign], Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ([[VAR_DECL] -> CASLFORMULA -> CASLFORMULA
forall f. [VAR_DECL] -> FORMULA f -> FORMULA f
mkForall [Int -> VAR_DECL
thingDecl Int
a, Int -> VAR_DECL
dataDecl Int
b] (CASLFORMULA -> CASLFORMULA) -> CASLFORMULA -> CASLFORMULA
forall a b. (a -> b) -> a -> b
$ [CASLFORMULA] -> CASLFORMULA -> CASLFORMULA
forall f. [FORMULA f] -> FORMULA f -> FORMULA f
implConj
            [Int -> TERM () -> CASLFORMULA
forall f. Int -> TERM f -> FORMULA f
mkEqDecl Int
a TERM ()
inS, VAR_DECL -> TERM () -> CASLFORMULA
forall f. VAR_DECL -> TERM f -> FORMULA f
mkEqVar (Int -> VAR_DECL
dataDecl Int
b) (TERM () -> CASLFORMULA) -> TERM () -> CASLFORMULA
forall a b. (a -> b) -> a -> b
$ TERM () -> SORT -> TERM ()
upcast TERM ()
inT SORT
dataS] CASLFORMULA
oProp],
            [], Int
startVar)

    BuiltInAtom iri :: IRI
iri args :: [DataArg]
args -> do
        [TERM ()]
prdArgs <- (DataArg -> Result (TERM ())) -> [DataArg] -> Result [TERM ()]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM DataArg -> Result (TERM ())
dArgToTerm [DataArg]
args
        let predtype :: PredType
predtype = [SORT] -> PredType
PredType ([SORT] -> PredType) -> [SORT] -> PredType
forall a b. (a -> b) -> a -> b
$ (DataArg -> SORT) -> [DataArg] -> [SORT]
forall a b. (a -> b) -> [a] -> [b]
map (SORT -> DataArg -> SORT
forall a b. a -> b -> a
const SORT
thing) [DataArg]
args
            prd :: CASLFORMULA
prd = PredType -> [TERM ()] -> SORT -> CASLFORMULA
forall f. PredType -> [TERM f] -> SORT -> FORMULA f
mkPred PredType
predtype [TERM ()]
prdArgs (IRI -> SORT
uriToId IRI
iri)

        ([CASLFORMULA], [CASLSign], Int)
-> Result ([CASLFORMULA], [CASLSign], Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ([CASLFORMULA
prd], [], Int
startVar)

    SameIndividualAtom iarg1 :: IndividualArg
iarg1 iarg2 :: IndividualArg
iarg2 -> do
            [CASLFORMULA]
fs <- SameOrDifferent -> Maybe IRI -> [IRI] -> Result [CASLFORMULA]
mapComIndivList SameOrDifferent
Same (IRI -> Maybe IRI
forall a. a -> Maybe a
Just (IRI -> Maybe IRI) -> IRI -> Maybe IRI
forall a b. (a -> b) -> a -> b
$ IndividualArg -> IRI
iArgToIRI IndividualArg
iarg1) [IndividualArg -> IRI
iArgToIRI IndividualArg
iarg2]
            ([CASLFORMULA], [CASLSign], Int)
-> Result ([CASLFORMULA], [CASLSign], Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ([CASLFORMULA]
fs, [], Int
startVar)
        
    DifferentIndividualsAtom iarg1 :: IndividualArg
iarg1 iarg2 :: IndividualArg
iarg2 -> do
            [CASLFORMULA]
fs <- SameOrDifferent -> Maybe IRI -> [IRI] -> Result [CASLFORMULA]
mapComIndivList SameOrDifferent
Different (IRI -> Maybe IRI
forall a. a -> Maybe a
Just (IRI -> Maybe IRI) -> IRI -> Maybe IRI
forall a b. (a -> b) -> a -> b
$ IndividualArg -> IRI
iArgToIRI IndividualArg
iarg1) [IndividualArg -> IRI
iArgToIRI IndividualArg
iarg2]
            ([CASLFORMULA], [CASLSign], Int)
-> Result ([CASLFORMULA], [CASLSign], Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ([CASLFORMULA]
fs, [], Int
startVar)
    _ -> String -> Result ([CASLFORMULA], [CASLSign], Int)
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail (String -> Result ([CASLFORMULA], [CASLSign], Int))
-> String -> Result ([CASLFORMULA], [CASLSign], Int)
forall a b. (a -> b) -> a -> b
$ "Couldn't translate unknown atom '" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Atom -> String
forall a. Show a => a -> String
show Atom
atom String -> ShowS
forall a. [a] -> [a] -> [a]
++ "'!"