{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances #-}
{- |
Module      :  ./OWL2/OWL22CommonLogic.hs
Description :  Comorphism from OWL2 to Common Logic
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)

a comorphism from OWL2 to CommonLogic
-}

module OWL2.OWL22CommonLogic (OWL22CommonLogic (..)) where

import Logic.Logic as Logic
import Logic.Comorphism
import qualified Common.AS_Annotation as CommonAnno
import Common.Result
import Control.Monad
import Data.Char
import Data.Either
import Data.Maybe
import qualified Data.Set as Set
import qualified Data.Map as Map

-- OWL2 = domain
import OWL2.Logic_OWL2
import OWL2.AS
import Common.IRI
import OWL2.Keywords
import OWL2.ProfilesAndSublogics
import OWL2.Morphism
import OWL2.Symbols hiding (idToRaw)
import qualified OWL2.Sign as OS
-- CommonLogic = codomain
import CommonLogic.Logic_CommonLogic
import Common.Id as Id
import CommonLogic.AS_CommonLogic
import CommonLogic.Sign
import CommonLogic.Symbol
import qualified CommonLogic.Morphism as CLM
import qualified CommonLogic.Sublogic as ClSl

import Common.ProofTree

data OWL22CommonLogic = OWL22CommonLogic deriving Int -> OWL22CommonLogic -> ShowS
[OWL22CommonLogic] -> ShowS
OWL22CommonLogic -> String
(Int -> OWL22CommonLogic -> ShowS)
-> (OWL22CommonLogic -> String)
-> ([OWL22CommonLogic] -> ShowS)
-> Show OWL22CommonLogic
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [OWL22CommonLogic] -> ShowS
$cshowList :: [OWL22CommonLogic] -> ShowS
show :: OWL22CommonLogic -> String
$cshow :: OWL22CommonLogic -> String
showsPrec :: Int -> OWL22CommonLogic -> ShowS
$cshowsPrec :: Int -> OWL22CommonLogic -> ShowS
Show

instance Language OWL22CommonLogic

instance Comorphism
    OWL22CommonLogic        -- 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
    CommonLogic             -- lid codomain
    ClSl.CommonLogicSL      -- sublogics codomain
    BASIC_SPEC              -- Basic spec codomain
    TEXT_META               -- sentence codomain
    SYMB_ITEMS              -- symbol items codomain
    SYMB_MAP_ITEMS          -- symbol map items codomain
    Sign                    -- signature codomain
    CLM.Morphism            -- morphism codomain
    Symbol                  -- symbol codomain
    Symbol                  -- rawsymbol codomain
    ProofTree               -- proof tree domain
    where
      sourceLogic :: OWL22CommonLogic -> OWL2
sourceLogic OWL22CommonLogic = OWL2
OWL2
      sourceSublogic :: OWL22CommonLogic -> ProfSub
sourceSublogic OWL22CommonLogic = ProfSub
topS
      targetLogic :: OWL22CommonLogic -> CommonLogic
targetLogic OWL22CommonLogic = CommonLogic
CommonLogic
      mapSublogic :: OWL22CommonLogic -> ProfSub -> Maybe CommonLogicSL
mapSublogic OWL22CommonLogic _ = CommonLogicSL -> Maybe CommonLogicSL
forall a. a -> Maybe a
Just CommonLogicSL
ClSl.top
      -- map_theory is not needed when mapMarkedTheory is defined
      map_theory :: OWL22CommonLogic
-> (Sign, [Named Axiom]) -> Result (Sign, [Named TEXT_META])
map_theory OWL22CommonLogic = String -> (Sign, [Named Axiom]) -> Result (Sign, [Named TEXT_META])
forall a. HasCallStack => String -> a
error "map_theory OWL22CommonLogic"
      mapMarkedTheory :: OWL22CommonLogic
-> (Sign, [Named Axiom]) -> Result (Sign, [Named TEXT_META])
mapMarkedTheory OWL22CommonLogic = (Sign, [Named Axiom]) -> Result (Sign, [Named TEXT_META])
mapTheory
      map_morphism :: OWL22CommonLogic -> OWLMorphism -> Result Morphism
map_morphism OWL22CommonLogic = OWLMorphism -> Result Morphism
mapMorphism
      map_symbol :: OWL22CommonLogic -> Sign -> Entity -> Set Symbol
map_symbol OWL22CommonLogic _ = Entity -> Set Symbol
mapSymbol
      isInclusionComorphism :: OWL22CommonLogic -> Bool
isInclusionComorphism OWL22CommonLogic = Bool
True
      has_model_expansion :: OWL22CommonLogic -> Bool
has_model_expansion OWL22CommonLogic = Bool
True

-- s = emptySig

smap :: Monad m =>
        (t4 -> t -> t1 -> t2 -> m t3) -> t4 -> t -> t1 -> t2 -> m (t3, t4)
smap :: (t4 -> t -> t1 -> t2 -> m t3) -> t4 -> t -> t1 -> t2 -> m (t3, t4)
smap f :: t4 -> t -> t1 -> t2 -> m t3
f s :: t4
s a :: t
a b :: t1
b c :: t2
c = do
    t3
x <- t4 -> t -> t1 -> t2 -> m t3
f t4
s t
a t1
b t2
c
    (t3, t4) -> m (t3, t4)
forall (m :: * -> *) a. Monad m => a -> m a
return (t3
x, t4
s)

hetsPrefix :: String
hetsPrefix :: String
hetsPrefix = ""

voiToTok :: VarOrIndi -> Token
voiToTok :: VarOrIndi -> Token
voiToTok v :: VarOrIndi
v = case VarOrIndi
v of
    OVar o :: Int
o -> Int -> Token
mkNName Int
o
    OIndi o :: IRI
o -> IRI -> Token
uriToTok IRI
o

varToInt :: VarOrIndi -> Int
varToInt :: VarOrIndi -> Int
varToInt v :: VarOrIndi
v = case VarOrIndi
v of
    OVar i :: Int
i -> Int
i
    _ -> String -> Int
forall a. HasCallStack => String -> a
error (String -> Int) -> String -> Int
forall a b. (a -> b) -> a -> b
$ "could not translate " String -> ShowS
forall a. [a] -> [a] -> [a]
++ VarOrIndi -> String
forall a. Show a => a -> String
show VarOrIndi
v

uriToTokM :: IRI -> Result Token
uriToTokM :: IRI -> Result Token
uriToTokM = Token -> Result Token
forall (m :: * -> *) a. Monad m => a -> m a
return (Token -> Result Token) -> (IRI -> Token) -> IRI -> Result Token
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IRI -> Token
uriToTok

mkBools :: BOOL_SENT -> SENTENCE
mkBools :: BOOL_SENT -> SENTENCE
mkBools bs :: BOOL_SENT
bs = BOOL_SENT -> Range -> SENTENCE
Bool_sent BOOL_SENT
bs Range
nullRange

mkAtoms :: ATOM -> SENTENCE
mkAtoms :: ATOM -> SENTENCE
mkAtoms as :: ATOM
as = ATOM -> Range -> SENTENCE
Atom_sent ATOM
as Range
nullRange

mkUnivQ :: [NAME_OR_SEQMARK] -> SENTENCE -> Id.Range -> SENTENCE
mkUnivQ :: [NAME_OR_SEQMARK] -> SENTENCE -> Range -> SENTENCE
mkUnivQ = QUANT -> [NAME_OR_SEQMARK] -> SENTENCE -> Range -> SENTENCE
Quant_sent QUANT
Universal

mkExist :: [NAME_OR_SEQMARK] -> SENTENCE -> Id.Range -> SENTENCE
mkExist :: [NAME_OR_SEQMARK] -> SENTENCE -> Range -> SENTENCE
mkExist = QUANT -> [NAME_OR_SEQMARK] -> SENTENCE -> Range -> SENTENCE
Quant_sent QUANT
Existential

cnjct :: [SENTENCE] -> BOOL_SENT
cnjct :: [SENTENCE] -> BOOL_SENT
cnjct = AndOr -> [SENTENCE] -> BOOL_SENT
Junction AndOr
Conjunction

dsjct :: [SENTENCE] -> BOOL_SENT
dsjct :: [SENTENCE] -> BOOL_SENT
dsjct = AndOr -> [SENTENCE] -> BOOL_SENT
Junction AndOr
Disjunction

mkNeg :: SENTENCE -> BOOL_SENT
mkNeg :: SENTENCE -> BOOL_SENT
mkNeg = SENTENCE -> BOOL_SENT
Negation

mkImpl :: SENTENCE -> SENTENCE -> BOOL_SENT
mkImpl :: SENTENCE -> SENTENCE -> BOOL_SENT
mkImpl = ImplEq -> SENTENCE -> SENTENCE -> BOOL_SENT
BinOp ImplEq
Implication

mkBicnd :: SENTENCE -> SENTENCE -> BOOL_SENT
mkBicnd :: SENTENCE -> SENTENCE -> BOOL_SENT
mkBicnd = ImplEq -> SENTENCE -> SENTENCE -> BOOL_SENT
BinOp ImplEq
Biconditional

mkNAME :: Int -> NAME_OR_SEQMARK
mkNAME :: Int -> NAME_OR_SEQMARK
mkNAME n :: Int
n = Token -> NAME_OR_SEQMARK
Name (Int -> Token
mkNName Int
n)

mkNTERM :: Int -> TERM
mkNTERM :: Int -> TERM
mkNTERM n :: Int
n = Token -> TERM
Name_term (Int -> Token
mkNName Int
n)

mkVTerm :: VarOrIndi -> TERM
mkVTerm :: VarOrIndi -> TERM
mkVTerm = Token -> TERM
Name_term (Token -> TERM) -> (VarOrIndi -> Token) -> VarOrIndi -> TERM
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VarOrIndi -> Token
voiToTok

mkTermSeq :: NAME -> TERM_SEQ
mkTermSeq :: Token -> TERM_SEQ
mkTermSeq = TERM -> TERM_SEQ
Term_seq (TERM -> TERM_SEQ) -> (Token -> TERM) -> Token -> TERM_SEQ
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Token -> TERM
Name_term

senToText :: SENTENCE -> TEXT
senToText :: SENTENCE -> TEXT
senToText s :: SENTENCE
s = [PHRASE] -> Range -> TEXT
Text [SENTENCE -> PHRASE
Sentence SENTENCE
s] Range
nullRange

msen2Txt :: [SENTENCE] -> [TEXT]
msen2Txt :: [SENTENCE] -> [TEXT]
msen2Txt = (SENTENCE -> TEXT) -> [SENTENCE] -> [TEXT]
forall a b. (a -> b) -> [a] -> [b]
map SENTENCE -> TEXT
senToText

mk1NTERM :: TERM
mk1NTERM :: TERM
mk1NTERM = Int -> TERM
mkNTERM 1

mk1NAME :: NAME_OR_SEQMARK
mk1NAME :: NAME_OR_SEQMARK
mk1NAME = Int -> NAME_OR_SEQMARK
mkNAME 1

mk1QU :: SENTENCE -> SENTENCE
mk1QU :: SENTENCE -> SENTENCE
mk1QU s :: SENTENCE
s = [NAME_OR_SEQMARK] -> SENTENCE -> Range -> SENTENCE
mkUnivQ [NAME_OR_SEQMARK
mk1NAME] SENTENCE
s Range
nullRange

mkQU :: [NAME_OR_SEQMARK] -> SENTENCE -> SENTENCE
mkQU :: [NAME_OR_SEQMARK] -> SENTENCE -> SENTENCE
mkQU l :: [NAME_OR_SEQMARK]
l s :: SENTENCE
s = [NAME_OR_SEQMARK] -> SENTENCE -> Range -> SENTENCE
mkUnivQ [NAME_OR_SEQMARK]
l SENTENCE
s Range
nullRange

mkBI :: SENTENCE -> SENTENCE -> SENTENCE
mkBI :: SENTENCE -> SENTENCE -> SENTENCE
mkBI s :: SENTENCE
s = BOOL_SENT -> SENTENCE
mkBools (BOOL_SENT -> SENTENCE)
-> (SENTENCE -> BOOL_SENT) -> SENTENCE -> SENTENCE
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SENTENCE -> SENTENCE -> BOOL_SENT
mkImpl SENTENCE
s

mkBN :: SENTENCE -> SENTENCE
mkBN :: SENTENCE -> SENTENCE
mkBN = BOOL_SENT -> SENTENCE
mkBools (BOOL_SENT -> SENTENCE)
-> (SENTENCE -> BOOL_SENT) -> SENTENCE -> SENTENCE
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SENTENCE -> BOOL_SENT
mkNeg

mkBD :: [SENTENCE] -> SENTENCE
mkBD :: [SENTENCE] -> SENTENCE
mkBD sl :: [SENTENCE]
sl = case [SENTENCE]
sl of
    [s :: SENTENCE
s] -> SENTENCE
s
    _ -> BOOL_SENT -> SENTENCE
mkBools (BOOL_SENT -> SENTENCE) -> BOOL_SENT -> SENTENCE
forall a b. (a -> b) -> a -> b
$ [SENTENCE] -> BOOL_SENT
dsjct [SENTENCE]
sl

mkBC :: [SENTENCE] -> SENTENCE
mkBC :: [SENTENCE] -> SENTENCE
mkBC sl :: [SENTENCE]
sl = case [SENTENCE]
sl of
    [s :: SENTENCE
s] -> SENTENCE
s
    _ -> BOOL_SENT -> SENTENCE
mkBools (BOOL_SENT -> SENTENCE) -> BOOL_SENT -> SENTENCE
forall a b. (a -> b) -> a -> b
$ [SENTENCE] -> BOOL_SENT
cnjct [SENTENCE]
sl

mkBB :: SENTENCE -> SENTENCE -> SENTENCE
mkBB :: SENTENCE -> SENTENCE -> SENTENCE
mkBB s :: SENTENCE
s = BOOL_SENT -> SENTENCE
mkBools (BOOL_SENT -> SENTENCE)
-> (SENTENCE -> BOOL_SENT) -> SENTENCE -> SENTENCE
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SENTENCE -> SENTENCE -> BOOL_SENT
mkBicnd SENTENCE
s

mkQE :: [NAME_OR_SEQMARK] -> SENTENCE -> SENTENCE
mkQE :: [NAME_OR_SEQMARK] -> SENTENCE -> SENTENCE
mkQE l :: [NAME_OR_SEQMARK]
l s :: SENTENCE
s = [NAME_OR_SEQMARK] -> SENTENCE -> Range -> SENTENCE
mkExist [NAME_OR_SEQMARK]
l SENTENCE
s Range
nullRange

mkAE :: TERM -> TERM -> SENTENCE
mkAE :: TERM -> TERM -> SENTENCE
mkAE t :: TERM
t = ATOM -> SENTENCE
mkAtoms (ATOM -> SENTENCE) -> (TERM -> ATOM) -> TERM -> SENTENCE
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TERM -> TERM -> ATOM
Equation TERM
t

mkEqual :: NAME -> NAME -> SENTENCE
mkEqual :: Token -> Token -> SENTENCE
mkEqual t1 :: Token
t1 t2 :: Token
t2 = TERM -> TERM -> SENTENCE
mkAE (Token -> TERM
Name_term Token
t1) (TERM -> SENTENCE) -> TERM -> SENTENCE
forall a b. (a -> b) -> a -> b
$ Token -> TERM
Name_term Token
t2

mkSent :: [NAME_OR_SEQMARK] -> [NAME_OR_SEQMARK] -> SENTENCE -> SENTENCE
       -> SENTENCE
mkSent :: [NAME_OR_SEQMARK]
-> [NAME_OR_SEQMARK] -> SENTENCE -> SENTENCE -> SENTENCE
mkSent l1 :: [NAME_OR_SEQMARK]
l1 l2 :: [NAME_OR_SEQMARK]
l2 s :: SENTENCE
s = [NAME_OR_SEQMARK] -> SENTENCE -> SENTENCE
mkQU [NAME_OR_SEQMARK]
l1 (SENTENCE -> SENTENCE)
-> (SENTENCE -> SENTENCE) -> SENTENCE -> SENTENCE
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [NAME_OR_SEQMARK] -> SENTENCE -> SENTENCE
mkQE [NAME_OR_SEQMARK]
l2 (SENTENCE -> SENTENCE)
-> (SENTENCE -> SENTENCE) -> SENTENCE -> SENTENCE
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SENTENCE -> SENTENCE -> SENTENCE
mkBI SENTENCE
s

mkQUBI :: [NAME_OR_SEQMARK] -> [SENTENCE] -> TERM -> TERM -> TEXT
mkQUBI :: [NAME_OR_SEQMARK] -> [SENTENCE] -> TERM -> TERM -> TEXT
mkQUBI l1 :: [NAME_OR_SEQMARK]
l1 l2 :: [SENTENCE]
l2 a :: TERM
a b :: TERM
b = SENTENCE -> TEXT
senToText (SENTENCE -> TEXT) -> SENTENCE -> TEXT
forall a b. (a -> b) -> a -> b
$ [NAME_OR_SEQMARK] -> SENTENCE -> SENTENCE
mkQU [NAME_OR_SEQMARK]
l1 (SENTENCE -> SENTENCE) -> SENTENCE -> SENTENCE
forall a b. (a -> b) -> a -> b
$ SENTENCE -> SENTENCE -> SENTENCE
mkBI ([SENTENCE] -> SENTENCE
mkBC [SENTENCE]
l2) (SENTENCE -> SENTENCE) -> SENTENCE -> SENTENCE
forall a b. (a -> b) -> a -> b
$ TERM -> TERM -> SENTENCE
mkAE TERM
a TERM
b

mkTermAtoms :: NAME -> [TERM] -> SENTENCE
mkTermAtoms :: Token -> [TERM] -> SENTENCE
mkTermAtoms ur :: Token
ur tl :: [TERM]
tl = ATOM -> SENTENCE
mkAtoms (ATOM -> SENTENCE) -> ATOM -> SENTENCE
forall a b. (a -> b) -> a -> b
$ TERM -> [TERM_SEQ] -> ATOM
Atom (Token -> TERM
Name_term Token
ur) ([TERM_SEQ] -> ATOM) -> [TERM_SEQ] -> ATOM
forall a b. (a -> b) -> a -> b
$ (TERM -> TERM_SEQ) -> [TERM] -> [TERM_SEQ]
forall a b. (a -> b) -> [a] -> [b]
map TERM -> TERM_SEQ
Term_seq [TERM]
tl

mk1TermAtom :: NAME -> SENTENCE
mk1TermAtom :: Token -> SENTENCE
mk1TermAtom ur :: Token
ur = Token -> [TERM] -> SENTENCE
mkTermAtoms Token
ur [TERM
mk1NTERM]

mkSAtom :: String -> SENTENCE
mkSAtom :: String -> SENTENCE
mkSAtom = Token -> SENTENCE
mk1TermAtom (Token -> SENTENCE) -> (String -> Token) -> String -> SENTENCE
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Token
mkSimpleId

sHead :: [SENTENCE] -> SENTENCE
sHead :: [SENTENCE] -> SENTENCE
sHead s :: [SENTENCE]
s = case [SENTENCE]
s of
    [a :: SENTENCE
a] -> SENTENCE
a
    _ -> [SENTENCE] -> SENTENCE
mkBC [SENTENCE]
s

eqFB :: [Int] -> [SENTENCE] -> TEXT
eqFB :: [Int] -> [SENTENCE] -> TEXT
eqFB nl :: [Int]
nl l :: [SENTENCE]
l = SENTENCE -> TEXT
senToText (SENTENCE -> TEXT) -> SENTENCE -> TEXT
forall a b. (a -> b) -> a -> b
$ [NAME_OR_SEQMARK] -> SENTENCE -> SENTENCE
mkQU ((Int -> NAME_OR_SEQMARK) -> [Int] -> [NAME_OR_SEQMARK]
forall a b. (a -> b) -> [a] -> [b]
map Int -> NAME_OR_SEQMARK
mkNAME [Int]
nl) (SENTENCE -> SENTENCE) -> SENTENCE -> SENTENCE
forall a b. (a -> b) -> a -> b
$ [SENTENCE] -> SENTENCE
sHead [SENTENCE]
l

mkNNameH :: Int -> String
mkNNameH :: Int -> String
mkNNameH k :: Int
k = case Int
k of
    0 -> ""
    j :: Int
j -> Int -> String
mkNNameH (Int
j Int -> Int -> Int
forall a. Integral a => a -> a -> a
`div` 26) String -> ShowS
forall a. [a] -> [a] -> [a]
++ [Int -> Char
chr (Int -> Char) -> Int -> Char
forall a b. (a -> b) -> a -> b
$ Int
j Int -> Int -> Int
forall a. Integral a => a -> a -> a
`mod` 26 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 96]

-- | Build a name
mkNName :: Int -> Token
mkNName :: Int -> Token
mkNName i :: Int
i = String -> Token
mkSimpleId (String -> Token) -> String -> Token
forall a b. (a -> b) -> a -> b
$ String
hetsPrefix String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
mkNNameH Int
i

-- | 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 t1. t -> [t1] -> [(t, t1)]
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 -> [t1] -> [(t, t1)]
mkPairs :: t -> [t1] -> [(t, t1)]
mkPairs a :: t
a = (t1 -> (t, t1)) -> [t1] -> [(t, t1)]
forall a b. (a -> b) -> [a] -> [b]
map (\ b :: t1
b -> (t
a, t1
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

-- | Mapping of OWL morphisms to CommonLogic morphisms
mapMorphism :: OWLMorphism -> Result CLM.Morphism
mapMorphism :: OWLMorphism -> Result Morphism
mapMorphism oMor :: OWLMorphism
oMor = do
    Sign
dm <- Sign -> Result Sign
mapSign (Sign -> Result Sign) -> Sign -> Result Sign
forall a b. (a -> b) -> a -> b
$ OWLMorphism -> Sign
osource OWLMorphism
oMor
    Sign
cd <- Sign -> Result Sign
mapSign (Sign -> Result Sign) -> Sign -> Result Sign
forall a b. (a -> b) -> a -> b
$ OWLMorphism -> Sign
otarget OWLMorphism
oMor
    Map Id Id
mapp <- Map Entity IRI -> Result (Map Id Id)
mapMap (Map Entity IRI -> Result (Map Id Id))
-> Map Entity IRI -> Result (Map Id Id)
forall a b. (a -> b) -> a -> b
$ OWLMorphism -> Map Entity IRI
mmaps OWLMorphism
oMor
    Morphism -> Result Morphism
forall (m :: * -> *) a. Monad m => a -> m a
return (Sign -> Sign -> Map Id Id -> Morphism
CLM.mkMorphism Sign
dm Sign
cd Map Id Id
mapp)

mapMap :: Map.Map Entity IRI -> Result (Map.Map Id Id)
mapMap :: Map Entity IRI -> Result (Map Id Id)
mapMap m :: Map Entity IRI
m = Map Id Id -> Result (Map Id Id)
forall (m :: * -> *) a. Monad m => a -> m a
return (Map Id Id -> Result (Map Id Id))
-> Map Id Id -> Result (Map Id Id)
forall a b. (a -> b) -> a -> b
$ (IRI -> Id) -> Map Id IRI -> Map Id Id
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map IRI -> Id
uriToId (Map Id IRI -> Map Id Id) -> Map Id IRI -> Map Id Id
forall a b. (a -> b) -> a -> b
$ (Entity -> Id) -> Map Entity IRI -> Map Id IRI
forall k2 k1 a. Ord k2 => (k1 -> k2) -> Map k1 a -> Map k2 a
Map.mapKeys Entity -> Id
entityToId Map Entity IRI
m

mapSymbol :: Entity -> Set.Set Symbol
mapSymbol :: Entity -> Set Symbol
mapSymbol (Entity _ _ iri :: IRI
iri) = Symbol -> Set Symbol
forall a. a -> Set a
Set.singleton (Symbol -> Set Symbol) -> Symbol -> Set Symbol
forall a b. (a -> b) -> a -> b
$ Id -> Symbol
idToRaw (Id -> Symbol) -> Id -> Symbol
forall a b. (a -> b) -> a -> b
$ IRI -> Id
uriToId IRI
iri

mapSign :: OS.Sign -> Result Sign
mapSign :: Sign -> Result Sign
mapSign sig :: Sign
sig =
  let conc :: Set IRI
conc = [Set IRI] -> Set IRI
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions [ Sign -> Set IRI
OS.concepts Sign
sig
                        , Sign -> Set IRI
OS.datatypes Sign
sig
                        , Sign -> Set IRI
OS.objectProperties Sign
sig
                        , Sign -> Set IRI
OS.dataProperties Sign
sig
                        , Sign -> Set IRI
OS.annotationRoles Sign
sig
                        , Sign -> Set IRI
OS.individuals Sign
sig ]
      itms :: Set Id
itms = (IRI -> Id) -> Set IRI -> Set Id
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map IRI -> Id
uriToId Set IRI
conc
  in Sign -> Result Sign
forall (m :: * -> *) a. Monad m => a -> m a
return Sign
emptySig { discourseNames :: Set Id
discourseNames = Set Id
itms }

nothingSent :: CommonAnno.Named TEXT
nothingSent :: Named TEXT
nothingSent = String -> TEXT -> Named TEXT
forall a s. a -> s -> SenAttr s a
CommonAnno.makeNamed "" (TEXT -> Named TEXT) -> TEXT -> Named TEXT
forall a b. (a -> b) -> a -> b
$ SENTENCE -> TEXT
senToText (SENTENCE -> TEXT) -> SENTENCE -> TEXT
forall a b. (a -> b) -> a -> b
$ SENTENCE -> SENTENCE
mk1QU (SENTENCE -> SENTENCE) -> SENTENCE -> SENTENCE
forall a b. (a -> b) -> a -> b
$ SENTENCE -> SENTENCE
mkBN (SENTENCE -> SENTENCE) -> SENTENCE -> SENTENCE
forall a b. (a -> b) -> a -> b
$ String -> SENTENCE
mkSAtom
    "Nothing"

thingIncl :: IRI -> CommonAnno.Named TEXT
thingIncl :: IRI -> Named TEXT
thingIncl iri :: IRI
iri = String -> TEXT -> Named TEXT
forall a s. a -> s -> SenAttr s a
CommonAnno.makeNamed "" (TEXT -> Named TEXT) -> TEXT -> Named TEXT
forall a b. (a -> b) -> a -> b
$ SENTENCE -> TEXT
senToText
    (SENTENCE -> TEXT) -> SENTENCE -> TEXT
forall a b. (a -> b) -> a -> b
$ SENTENCE -> SENTENCE
mk1QU (SENTENCE -> SENTENCE) -> SENTENCE -> SENTENCE
forall a b. (a -> b) -> a -> b
$ SENTENCE -> SENTENCE -> SENTENCE
mkBI (Token -> SENTENCE
mk1TermAtom (Token -> SENTENCE) -> Token -> SENTENCE
forall a b. (a -> b) -> a -> b
$ IRI -> Token
uriToTok IRI
iri) (SENTENCE -> SENTENCE) -> SENTENCE -> SENTENCE
forall a b. (a -> b) -> a -> b
$ String -> SENTENCE
mkSAtom "Thing"

dataIncl :: IRI -> CommonAnno.Named TEXT
dataIncl :: IRI -> Named TEXT
dataIncl iri :: IRI
iri = String -> TEXT -> Named TEXT
forall a s. a -> s -> SenAttr s a
CommonAnno.makeNamed "" (TEXT -> Named TEXT) -> TEXT -> Named TEXT
forall a b. (a -> b) -> a -> b
$ SENTENCE -> TEXT
senToText
    (SENTENCE -> TEXT) -> SENTENCE -> TEXT
forall a b. (a -> b) -> a -> b
$ SENTENCE -> SENTENCE
mk1QU (SENTENCE -> SENTENCE) -> SENTENCE -> SENTENCE
forall a b. (a -> b) -> a -> b
$ SENTENCE -> SENTENCE -> SENTENCE
mkBI (Token -> SENTENCE
mk1TermAtom (Token -> SENTENCE) -> Token -> SENTENCE
forall a b. (a -> b) -> a -> b
$ IRI -> Token
uriToTok IRI
iri) (SENTENCE -> SENTENCE) -> SENTENCE -> SENTENCE
forall a b. (a -> b) -> a -> b
$ String -> SENTENCE
mkSAtom "Datatype"

propertyIncl :: String -> IRI -> CommonAnno.Named TEXT
propertyIncl :: String -> IRI -> Named TEXT
propertyIncl s :: String
s prop :: IRI
prop = String -> TEXT -> Named TEXT
forall a s. a -> s -> SenAttr s a
CommonAnno.makeNamed "" (TEXT -> Named TEXT) -> TEXT -> Named TEXT
forall a b. (a -> b) -> a -> b
$ SENTENCE -> TEXT
senToText (SENTENCE -> TEXT) -> SENTENCE -> TEXT
forall a b. (a -> b) -> a -> b
$
    let [d :: SENTENCE
d, pr :: SENTENCE
pr] = (Token -> SENTENCE) -> [Token] -> [SENTENCE]
forall a b. (a -> b) -> [a] -> [b]
map (Token -> [TERM] -> SENTENCE
`mkTermAtoms` (Int -> TERM) -> [Int] -> [TERM]
forall a b. (a -> b) -> [a] -> [b]
map Int -> TERM
mkNTERM [1, 2])
            [IRI -> Token
uriToTok IRI
prop, String -> Token
mkSimpleId String
s]
    in SENTENCE -> SENTENCE -> SENTENCE
mkBI SENTENCE
d (SENTENCE -> SENTENCE) -> SENTENCE -> SENTENCE
forall a b. (a -> b) -> a -> b
$ if String
s String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [String
topDataProp, String
topObjProp] then SENTENCE
pr else SENTENCE -> SENTENCE
mkBN SENTENCE
pr

declarations :: OS.Sign -> [CommonAnno.Named TEXT]
declarations :: Sign -> [Named TEXT]
declarations s :: Sign
s =
    let c :: [IRI]
c = Set IRI -> [IRI]
forall a. Set a -> [a]
Set.toList (Set IRI -> [IRI]) -> Set IRI -> [IRI]
forall a b. (a -> b) -> a -> b
$ Sign -> Set IRI
OS.concepts Sign
s
        dt :: [IRI]
dt = Set IRI -> [IRI]
forall a. Set a -> [a]
Set.toList (Set IRI -> [IRI]) -> Set IRI -> [IRI]
forall a b. (a -> b) -> a -> b
$ Sign -> Set IRI
OS.datatypes Sign
s
        dp :: [IRI]
dp = Set IRI -> [IRI]
forall a. Set a -> [a]
Set.toList (Set IRI -> [IRI]) -> Set IRI -> [IRI]
forall a b. (a -> b) -> a -> b
$ Sign -> Set IRI
OS.dataProperties Sign
s
        op :: [IRI]
op = Set IRI -> [IRI]
forall a. Set a -> [a]
Set.toList (Set IRI -> [IRI]) -> Set IRI -> [IRI]
forall a b. (a -> b) -> a -> b
$ Sign -> Set IRI
OS.objectProperties Sign
s
    in (IRI -> Named TEXT) -> [IRI] -> [Named TEXT]
forall a b. (a -> b) -> [a] -> [b]
map IRI -> Named TEXT
thingIncl [IRI]
c
        [Named TEXT] -> [Named TEXT] -> [Named TEXT]
forall a. [a] -> [a] -> [a]
++ (IRI -> Named TEXT) -> [IRI] -> [Named TEXT]
forall a b. (a -> b) -> [a] -> [b]
map IRI -> Named TEXT
dataIncl ((String -> IRI) -> [String] -> [IRI]
forall a b. (a -> b) -> [a] -> [b]
map (String -> String -> IRI
mkAbbrevIRI "xsd") [String]
datatypeKeys [IRI] -> [IRI] -> [IRI]
forall a. [a] -> [a] -> [a]
++ [IRI]
dt)
        [Named TEXT] -> [Named TEXT] -> [Named TEXT]
forall a. [a] -> [a] -> [a]
++ (IRI -> Named TEXT) -> [IRI] -> [Named TEXT]
forall a b. (a -> b) -> [a] -> [b]
map (String -> IRI -> Named TEXT
propertyIncl String
topDataProp) [IRI]
dp
        [Named TEXT] -> [Named TEXT] -> [Named TEXT]
forall a. [a] -> [a] -> [a]
++ (IRI -> Named TEXT) -> [IRI] -> [Named TEXT]
forall a b. (a -> b) -> [a] -> [b]
map (String -> IRI -> Named TEXT
propertyIncl String
bottomDataProp) [IRI]
dp
        [Named TEXT] -> [Named TEXT] -> [Named TEXT]
forall a. [a] -> [a] -> [a]
++ (IRI -> Named TEXT) -> [IRI] -> [Named TEXT]
forall a b. (a -> b) -> [a] -> [b]
map (String -> IRI -> Named TEXT
propertyIncl String
topObjProp) [IRI]
op
        [Named TEXT] -> [Named TEXT] -> [Named TEXT]
forall a. [a] -> [a] -> [a]
++ (IRI -> Named TEXT) -> [IRI] -> [Named TEXT]
forall a b. (a -> b) -> [a] -> [b]
map (String -> IRI -> Named TEXT
propertyIncl String
bottomObjProp) [IRI]
op

thingDataDisjoint :: CommonAnno.Named TEXT
thingDataDisjoint :: Named TEXT
thingDataDisjoint = String -> TEXT -> Named TEXT
forall a s. a -> s -> SenAttr s a
CommonAnno.makeNamed "" (TEXT -> Named TEXT) -> TEXT -> Named TEXT
forall a b. (a -> b) -> a -> b
$ SENTENCE -> TEXT
senToText (SENTENCE -> TEXT) -> SENTENCE -> TEXT
forall a b. (a -> b) -> a -> b
$ SENTENCE -> SENTENCE
mk1QU (SENTENCE -> SENTENCE) -> SENTENCE -> SENTENCE
forall a b. (a -> b) -> a -> b
$ SENTENCE -> SENTENCE
mkBN
    (SENTENCE -> SENTENCE) -> SENTENCE -> SENTENCE
forall a b. (a -> b) -> a -> b
$ [SENTENCE] -> SENTENCE
mkBC ([SENTENCE] -> SENTENCE) -> [SENTENCE] -> SENTENCE
forall a b. (a -> b) -> a -> b
$ (String -> SENTENCE) -> [String] -> [SENTENCE]
forall a b. (a -> b) -> [a] -> [b]
map String -> SENTENCE
mkSAtom ["Thing", "Datatype"]

mapTheory :: (OS.Sign, [CommonAnno.Named Axiom])
             -> Result (Sign, [CommonAnno.Named TEXT_META])
mapTheory :: (Sign, [Named Axiom]) -> Result (Sign, [Named TEXT_META])
mapTheory (owlSig :: Sign
owlSig, owlSens :: [Named Axiom]
owlSens) = do
    Sign
cSig <- Sign -> Result Sign
mapSign Sign
owlSig
    (cSensI :: [Named TEXT]
cSensI, nSig :: Sign
nSig) <- (([Named TEXT], Sign)
 -> Named Axiom -> Result ([Named TEXT], Sign))
-> ([Named TEXT], Sign)
-> [Named Axiom]
-> Result ([Named TEXT], Sign)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (\ (x :: [Named TEXT]
x, y :: Sign
y) z :: Named Axiom
z ->
              do
                (sen :: [Named TEXT]
sen, sig :: Sign
sig) <- Sign -> Named Axiom -> Result ([Named TEXT], Sign)
mapSentence Sign
y Named Axiom
z
                ([Named TEXT], Sign) -> Result ([Named TEXT], Sign)
forall (m :: * -> *) a. Monad m => a -> m a
return ([Named TEXT]
x [Named TEXT] -> [Named TEXT] -> [Named TEXT]
forall a. [a] -> [a] -> [a]
++ [Named TEXT]
sen, Sign -> Sign -> Sign
unite Sign
sig Sign
y)
                ) ([], Sign
cSig) [Named Axiom]
owlSens
    let sig :: Sign
sig = Sign -> Sign -> Sign
unite (Sign
emptySig {discourseNames :: Set Id
discourseNames = [Id] -> Set Id
forall a. Ord a => [a] -> Set a
Set.fromList ([Id] -> Set Id) -> [Id] -> Set Id
forall a b. (a -> b) -> a -> b
$ (String -> Id) -> [String] -> [Id]
forall a b. (a -> b) -> [a] -> [b]
map (IRI -> Id
uriToId (IRI -> Id) -> (String -> IRI) -> String -> Id
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
            IRI -> IRI
setReservedPrefix (IRI -> IRI) -> (String -> IRI) -> String -> IRI
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> IRI
mkIRI) ([String] -> [Id]) -> [String] -> [Id]
forall a b. (a -> b) -> a -> b
$ "Datatype" String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [String]
predefClass
            [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String
topDataProp, String
bottomDataProp, String
topObjProp, String
bottomObjProp]
            [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String]
datatypeKeys}) Sign
nSig
        cSens :: [Named TEXT]
cSens = (Named TEXT -> Named TEXT) -> [Named TEXT] -> [Named TEXT]
forall a b. (a -> b) -> [a] -> [b]
map (String -> Named TEXT -> Named TEXT
forall s. String -> Named s -> Named s
CommonAnno.markSen "OWLbuiltin")
                  [Named TEXT
nothingSent, Named TEXT
thingDataDisjoint]
                [Named TEXT] -> [Named TEXT] -> [Named TEXT]
forall a. [a] -> [a] -> [a]
++ (Named TEXT -> Named TEXT) -> [Named TEXT] -> [Named TEXT]
forall a b. (a -> b) -> [a] -> [b]
map (String -> Named TEXT -> Named TEXT
forall s. String -> Named s -> Named s
CommonAnno.markSen "OWLsign") (Sign -> [Named TEXT]
declarations Sign
owlSig)
                [Named TEXT] -> [Named TEXT] -> [Named TEXT]
forall a. [a] -> [a] -> [a]
++ (Named TEXT -> Named TEXT) -> [Named TEXT] -> [Named TEXT]
forall a b. (a -> b) -> [a] -> [b]
map (String -> Named TEXT -> Named TEXT
forall s. String -> Named s -> Named s
CommonAnno.markSen "OWLsen") [Named TEXT]
cSensI
    (Sign, [Named TEXT_META]) -> Result (Sign, [Named TEXT_META])
forall (m :: * -> *) a. Monad m => a -> m a
return (Sign
sig, (Named TEXT -> Named TEXT_META)
-> [Named TEXT] -> [Named TEXT_META]
forall a b. (a -> b) -> [a] -> [b]
map ((TEXT -> TEXT_META) -> Named TEXT -> Named TEXT_META
forall s t a. (s -> t) -> SenAttr s a -> SenAttr t a
CommonAnno.mapNamed TEXT -> TEXT_META
addMrs) [Named TEXT]
cSens)

-- | mapping of OWL to CommonLogic_DL formulae
mapSentence :: Sign                             -- ^ CommonLogic Signature
  -> CommonAnno.Named Axiom                     -- ^ OWL2 Sentence
  -> Result ([CommonAnno.Named TEXT], Sign)     -- ^ CommonLogic TEXT
mapSentence :: Sign -> Named Axiom -> Result ([Named TEXT], Sign)
mapSentence cSig :: Sign
cSig inSen :: Named Axiom
inSen = do
    (outAx :: [TEXT]
outAx, outSig :: Sign
outSig) <- Sign -> Axiom -> Result ([TEXT], Sign)
mapAxioms Sign
cSig (Axiom -> Result ([TEXT], Sign)) -> Axiom -> Result ([TEXT], Sign)
forall a b. (a -> b) -> a -> b
$ Named Axiom -> Axiom
forall s a. SenAttr s a -> s
CommonAnno.sentence Named Axiom
inSen
    ([Named TEXT], Sign) -> Result ([Named TEXT], Sign)
forall (m :: * -> *) a. Monad m => a -> m a
return ((TEXT -> Named TEXT) -> [TEXT] -> [Named TEXT]
forall a b. (a -> b) -> [a] -> [b]
map (((Axiom -> TEXT) -> Named Axiom -> Named TEXT)
-> Named Axiom -> (Axiom -> TEXT) -> Named TEXT
forall a b c. (a -> b -> c) -> b -> a -> c
flip (Axiom -> TEXT) -> Named Axiom -> Named TEXT
forall s t a. (s -> t) -> SenAttr s a -> SenAttr t a
CommonAnno.mapNamed Named Axiom
inSen ((Axiom -> TEXT) -> Named TEXT)
-> (TEXT -> Axiom -> TEXT) -> TEXT -> Named TEXT
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TEXT -> Axiom -> TEXT
forall a b. a -> b -> a
const) [TEXT]
outAx, Sign
outSig)

-- | Mapping of Class IRIs
mapClassIRI :: Sign -> Class -> Token -> Result SENTENCE
mapClassIRI :: Sign -> IRI -> Token -> Result SENTENCE
mapClassIRI _ c :: IRI
c tok :: Token
tok = (Token -> SENTENCE) -> Result Token -> Result SENTENCE
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Token -> [TERM] -> SENTENCE
`mkTermAtoms` [Token -> TERM
Name_term Token
tok]) (Result Token -> Result SENTENCE)
-> Result Token -> Result SENTENCE
forall a b. (a -> b) -> a -> b
$ IRI -> Result Token
uriToTokM IRI
c

-- | Mapping of Individual IRIs
mapIndivIRI :: Sign -> Individual -> Result TERM
mapIndivIRI :: Sign -> IRI -> Result TERM
mapIndivIRI _ i :: IRI
i = (Token -> TERM) -> Result Token -> Result TERM
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Token -> TERM
Name_term (Result Token -> Result TERM) -> Result Token -> Result TERM
forall a b. (a -> b) -> a -> b
$ IRI -> Result Token
uriToTokM IRI
i

-- | mapping of individual list
mapComIndivList :: Sign -> SameOrDifferent -> Maybe Individual -> [Individual]
                -> Result [SENTENCE]
mapComIndivList :: Sign -> SameOrDifferent -> Maybe IRI -> [IRI] -> Result [SENTENCE]
mapComIndivList cSig :: Sign
cSig sod :: SameOrDifferent
sod mi :: Maybe IRI
mi 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 (Sign -> IRI -> Result TERM
mapIndivIRI Sign
cSig) [IRI]
inds
    [(TERM, TERM)]
il <- case Maybe IRI
mi 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 i :: IRI
i -> (TERM -> [(TERM, TERM)]) -> Result TERM -> Result [(TERM, TERM)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (TERM -> [TERM] -> [(TERM, TERM)]
forall t t1. t -> [t1] -> [(t, t1)]
`mkPairs` [TERM]
fs) (Result TERM -> Result [(TERM, TERM)])
-> Result TERM -> Result [(TERM, TERM)]
forall a b. (a -> b) -> a -> b
$ Sign -> IRI -> Result TERM
mapIndivIRI Sign
cSig IRI
i
    let sntLst :: [SENTENCE]
sntLst = ((TERM, TERM) -> SENTENCE) -> [(TERM, TERM)] -> [SENTENCE]
forall a b. (a -> b) -> [a] -> [b]
map (\ (x :: TERM
x, y :: TERM
y) -> case SameOrDifferent
sod of
                    Same -> TERM -> TERM -> SENTENCE
mkAE TERM
x TERM
y
                    Different -> SENTENCE -> SENTENCE
mkBN (SENTENCE -> SENTENCE) -> SENTENCE -> SENTENCE
forall a b. (a -> b) -> a -> b
$ TERM -> TERM -> SENTENCE
mkAE TERM
x TERM
y) [(TERM, TERM)]
il
    [SENTENCE] -> Result [SENTENCE]
forall (m :: * -> *) a. Monad m => a -> m a
return [[SENTENCE] -> SENTENCE
mkBC [SENTENCE]
sntLst]

mapLitAux :: VarOrIndi -> Literal -> Result (Either (SENTENCE, SENTENCE) TERM)
mapLitAux :: VarOrIndi -> Literal -> Result (Either (SENTENCE, SENTENCE) TERM)
mapLitAux var :: VarOrIndi
var c :: Literal
c = Either (SENTENCE, SENTENCE) TERM
-> Result (Either (SENTENCE, SENTENCE) TERM)
forall (m :: * -> *) a. Monad m => a -> m a
return (Either (SENTENCE, SENTENCE) TERM
 -> Result (Either (SENTENCE, SENTENCE) TERM))
-> Either (SENTENCE, SENTENCE) TERM
-> Result (Either (SENTENCE, SENTENCE) TERM)
forall a b. (a -> b) -> a -> b
$ case Literal
c of
    Literal l :: String
l ty :: TypedOrUntyped
ty -> case TypedOrUntyped
ty of
        Typed dt :: IRI
dt -> (SENTENCE, SENTENCE) -> Either (SENTENCE, SENTENCE) TERM
forall a b. a -> Either a b
Left (Token -> Token -> SENTENCE
mkEqual (String -> Token
mkSimpleId String
l) (Token -> SENTENCE) -> Token -> SENTENCE
forall a b. (a -> b) -> a -> b
$ VarOrIndi -> Token
voiToTok VarOrIndi
var,
                    Token -> [TERM] -> SENTENCE
mkTermAtoms (IRI -> Token
uriToTok IRI
dt) [VarOrIndi -> TERM
mkVTerm VarOrIndi
var])
        Untyped _ -> TERM -> Either (SENTENCE, SENTENCE) TERM
forall a b. b -> Either a b
Right (TERM -> Either (SENTENCE, SENTENCE) TERM)
-> TERM -> Either (SENTENCE, SENTENCE) TERM
forall a b. (a -> b) -> a -> b
$ Token -> TERM
Name_term (Token -> TERM) -> Token -> TERM
forall a b. (a -> b) -> a -> b
$ String -> Token
mkSimpleId String
l
    NumberLit l :: FloatLit
l -> (SENTENCE, SENTENCE) -> Either (SENTENCE, SENTENCE) TERM
forall a b. a -> Either a b
Left (Token -> Token -> SENTENCE
mkEqual (String -> Token
mkSimpleId (String -> Token) -> String -> Token
forall a b. (a -> b) -> a -> b
$ FloatLit -> String
forall a. Show a => a -> String
show FloatLit
l) (Token -> SENTENCE) -> Token -> SENTENCE
forall a b. (a -> b) -> a -> b
$ VarOrIndi -> Token
voiToTok VarOrIndi
var,
                    Token -> [TERM] -> SENTENCE
mkTermAtoms (String -> Token
mkSimpleId (String -> Token) -> String -> Token
forall a b. (a -> b) -> a -> b
$ FloatLit -> String
numberName FloatLit
l) [VarOrIndi -> TERM
mkVTerm VarOrIndi
var])

mapLit :: Int -> Literal -> Result (Either (SENTENCE, SENTENCE) TERM)
mapLit :: Int -> Literal -> Result (Either (SENTENCE, SENTENCE) TERM)
mapLit i :: Int
i = VarOrIndi -> Literal -> Result (Either (SENTENCE, SENTENCE) TERM)
mapLitAux (Int -> VarOrIndi
OVar Int
i) 

-- | Mapping of data properties
mapDataProp :: Sign -> DataPropertyExpression -> VarOrIndi -> VarOrIndi
            -> Result SENTENCE
mapDataProp :: Sign -> IRI -> VarOrIndi -> VarOrIndi -> Result SENTENCE
mapDataProp _ dp :: IRI
dp a :: VarOrIndi
a b :: VarOrIndi
b = (Token -> SENTENCE) -> Result Token -> Result SENTENCE
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Token -> [TERM] -> SENTENCE
`mkTermAtoms` (VarOrIndi -> TERM) -> [VarOrIndi] -> [TERM]
forall a b. (a -> b) -> [a] -> [b]
map VarOrIndi -> TERM
mkVTerm [VarOrIndi
a, VarOrIndi
b])
    (Result Token -> Result SENTENCE)
-> Result Token -> Result SENTENCE
forall a b. (a -> b) -> a -> b
$ IRI -> Result Token
uriToTokM IRI
dp

mapDataPropI :: Sign -> VarOrIndi -> VarOrIndi -> DataPropertyExpression
             -> Result SENTENCE
mapDataPropI :: Sign -> VarOrIndi -> VarOrIndi -> IRI -> Result SENTENCE
mapDataPropI cSig :: Sign
cSig a :: VarOrIndi
a b :: VarOrIndi
b dp :: IRI
dp = Sign -> IRI -> VarOrIndi -> VarOrIndi -> Result SENTENCE
mapDataProp Sign
cSig IRI
dp VarOrIndi
a VarOrIndi
b

-- | Mapping of obj props
mapObjProp :: Sign -> ObjectPropertyExpression -> VarOrIndi -> VarOrIndi
            -> Result SENTENCE
mapObjProp :: Sign
-> ObjectPropertyExpression
-> VarOrIndi
-> VarOrIndi
-> Result SENTENCE
mapObjProp cSig :: Sign
cSig ob :: ObjectPropertyExpression
ob v1 :: VarOrIndi
v1 v2 :: VarOrIndi
v2 = case ObjectPropertyExpression
ob of
    ObjectProp u :: IRI
u -> (Token -> SENTENCE) -> Result Token -> Result SENTENCE
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Token -> [TERM] -> SENTENCE
`mkTermAtoms` (VarOrIndi -> TERM) -> [VarOrIndi] -> [TERM]
forall a b. (a -> b) -> [a] -> [b]
map VarOrIndi -> TERM
mkVTerm [VarOrIndi
v1, VarOrIndi
v2]) (Result Token -> Result SENTENCE)
-> Result Token -> Result SENTENCE
forall a b. (a -> b) -> a -> b
$ IRI -> Result Token
uriToTokM IRI
u
    ObjectInverseOf u :: ObjectPropertyExpression
u -> Sign
-> ObjectPropertyExpression
-> VarOrIndi
-> VarOrIndi
-> Result SENTENCE
mapObjProp Sign
cSig ObjectPropertyExpression
u VarOrIndi
v2 VarOrIndi
v1

mapDPE :: Sign -> DataPropertyExpression -> Int -> Int -> Result SENTENCE
mapDPE :: Sign -> IRI -> Int -> Int -> Result SENTENCE
mapDPE cSig :: Sign
cSig dpe :: IRI
dpe x :: Int
x y :: Int
y = Sign -> IRI -> VarOrIndi -> VarOrIndi -> Result SENTENCE
mapDataProp Sign
cSig IRI
dpe (Int -> VarOrIndi
OVar Int
x) (VarOrIndi -> Result SENTENCE) -> VarOrIndi -> Result SENTENCE
forall a b. (a -> b) -> a -> b
$ Int -> VarOrIndi
OVar Int
y

mapOPE :: Sign -> ObjectPropertyExpression -> Int -> Int -> Result SENTENCE
mapOPE :: Sign -> ObjectPropertyExpression -> Int -> Int -> Result SENTENCE
mapOPE cSig :: Sign
cSig ope :: ObjectPropertyExpression
ope x :: Int
x y :: Int
y = Sign
-> ObjectPropertyExpression
-> VarOrIndi
-> VarOrIndi
-> Result SENTENCE
mapObjProp Sign
cSig ObjectPropertyExpression
ope (Int -> VarOrIndi
OVar Int
x) (VarOrIndi -> Result SENTENCE) -> VarOrIndi -> Result SENTENCE
forall a b. (a -> b) -> a -> b
$ Int -> VarOrIndi
OVar Int
y

mapOPEList :: Sign -> Int -> Int -> [ObjectPropertyExpression]
    -> Result [SENTENCE]
mapOPEList :: Sign
-> Int -> Int -> [ObjectPropertyExpression] -> Result [SENTENCE]
mapOPEList s :: Sign
s a :: Int
a b :: Int
b = (ObjectPropertyExpression -> Result SENTENCE)
-> [ObjectPropertyExpression] -> Result [SENTENCE]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ((\ sig :: Sign
sig x1 :: Int
x1 x2 :: Int
x2 op :: ObjectPropertyExpression
op -> Sign -> ObjectPropertyExpression -> Int -> Int -> Result SENTENCE
mapOPE Sign
sig ObjectPropertyExpression
op Int
x1 Int
x2 ) Sign
s Int
a Int
b)

mapDPEList :: Sign -> Int -> Int -> [DataPropertyExpression]
    -> Result [SENTENCE]
mapDPEList :: Sign -> Int -> Int -> [IRI] -> Result [SENTENCE]
mapDPEList s :: Sign
s a :: Int
a b :: Int
b = (IRI -> Result SENTENCE) -> [IRI] -> Result [SENTENCE]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ((\ sig :: Sign
sig x1 :: Int
x1 x2 :: Int
x2 dp :: IRI
dp -> Sign -> IRI -> Int -> Int -> Result SENTENCE
mapDPE Sign
sig IRI
dp Int
x1 Int
x2 ) Sign
s Int
a Int
b)

mapObjPropListP :: Sign -> Int -> Int
    -> [(ObjectPropertyExpression, ObjectPropertyExpression)]
    -> Result [(SENTENCE, SENTENCE)]
mapObjPropListP :: Sign
-> Int
-> Int
-> [(ObjectPropertyExpression, ObjectPropertyExpression)]
-> Result [(SENTENCE, SENTENCE)]
mapObjPropListP = (Sign
 -> Int -> Int -> [ObjectPropertyExpression] -> Result [SENTENCE])
-> Sign
-> Int
-> Int
-> [(ObjectPropertyExpression, ObjectPropertyExpression)]
-> Result [(SENTENCE, SENTENCE)]
forall (m :: * -> *) t t1 t2 a b.
Monad m =>
(t -> t1 -> t2 -> [a] -> m [b])
-> t -> t1 -> t2 -> [(a, a)] -> m [(b, b)]
mapObjOrDataListP Sign
-> Int -> Int -> [ObjectPropertyExpression] -> Result [SENTENCE]
mapOPEList

mapDataPropListP :: Sign -> Int -> Int
    -> [(DataPropertyExpression, DataPropertyExpression)]
    -> Result [(SENTENCE, SENTENCE)]
mapDataPropListP :: Sign -> Int -> Int -> [(IRI, IRI)] -> Result [(SENTENCE, SENTENCE)]
mapDataPropListP = (Sign -> Int -> Int -> [IRI] -> Result [SENTENCE])
-> Sign
-> Int
-> Int
-> [(IRI, IRI)]
-> Result [(SENTENCE, SENTENCE)]
forall (m :: * -> *) t t1 t2 a b.
Monad m =>
(t -> t1 -> t2 -> [a] -> m [b])
-> t -> t1 -> t2 -> [(a, a)] -> m [(b, b)]
mapObjOrDataListP Sign -> Int -> Int -> [IRI] -> Result [SENTENCE]
mapDPEList

mapObjOrDataListP :: Monad m => (t -> t1 -> t2 -> [a] -> m [b]) -> t -> t1 -> t2
    -> [(a, a)] -> m [(b, b)]
mapObjOrDataListP :: (t -> t1 -> t2 -> [a] -> m [b])
-> t -> t1 -> t2 -> [(a, a)] -> m [(b, b)]
mapObjOrDataListP f :: t -> t1 -> t2 -> [a] -> m [b]
f cSig :: t
cSig a :: t1
a b :: t2
b ls :: [(a, a)]
ls = do
    let (l :: [a]
l, r :: [a]
r) = [(a, a)] -> ([a], [a])
forall a b. [(a, b)] -> ([a], [b])
unzip [(a, a)]
ls
    [b]
l1 <- t -> t1 -> t2 -> [a] -> m [b]
f t
cSig t1
a t2
b [a]
l
    [b]
l2 <- t -> t1 -> t2 -> [a] -> m [b]
f t
cSig t1
a t2
b [a]
r
    [(b, b)] -> m [(b, b)]
forall (m :: * -> *) a. Monad m => a -> m a
return ([(b, b)] -> m [(b, b)]) -> [(b, b)] -> m [(b, b)]
forall a b. (a -> b) -> a -> b
$ [b] -> [b] -> [(b, b)]
forall t t1. [t] -> [t1] -> [(t, t1)]
zip [b]
l1 [b]
l2

mapDataRange :: Sign -> DataRange -> VarOrIndi -> Result (SENTENCE, Sign)
mapDataRange :: Sign -> DataRange -> VarOrIndi -> Result (SENTENCE, Sign)
mapDataRange cSig :: Sign
cSig dr :: DataRange
dr var :: VarOrIndi
var = Sign -> DataRange -> VarOrIndi -> Int -> Result (SENTENCE, Sign)
mapDataRangeAux Sign
cSig DataRange
dr VarOrIndi
var (VarOrIndi -> Int
varToInt VarOrIndi
var Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1)


-- | mapping of Data Range
mapDataRangeAux :: Sign -> DataRange -> VarOrIndi -> Int -> Result (SENTENCE, Sign)
mapDataRangeAux :: Sign -> DataRange -> VarOrIndi -> Int -> Result (SENTENCE, Sign)
mapDataRangeAux cSig :: Sign
cSig dr :: DataRange
dr var :: VarOrIndi
var i :: Int
i = let uid :: TERM
uid = VarOrIndi -> TERM
mkVTerm VarOrIndi
var in case DataRange
dr of
    DataJunction jt :: JunctionType
jt drl :: [DataRange]
drl -> do
        (jl :: [SENTENCE]
jl, sig :: [Sign]
sig) <- (DataRange -> Result (SENTENCE, Sign))
-> [DataRange] -> Result ([SENTENCE], [Sign])
forall (m :: * -> *) a b c.
Applicative m =>
(a -> m (b, c)) -> [a] -> m ([b], [c])
mapAndUnzipM ((\ s :: Sign
s v :: VarOrIndi
v r :: DataRange
r -> Sign -> DataRange -> VarOrIndi -> Result (SENTENCE, Sign)
mapDataRange Sign
s DataRange
r VarOrIndi
v) Sign
cSig VarOrIndi
var) [DataRange]
drl
        let un :: Sign
un = [Sign] -> Sign
uniteL [Sign]
sig
        (SENTENCE, Sign) -> Result (SENTENCE, Sign)
forall (m :: * -> *) a. Monad m => a -> m a
return ((SENTENCE, Sign) -> Result (SENTENCE, Sign))
-> (SENTENCE, Sign) -> Result (SENTENCE, Sign)
forall a b. (a -> b) -> a -> b
$ case JunctionType
jt of
                IntersectionOf -> ([SENTENCE] -> SENTENCE
mkBC [SENTENCE]
jl, Sign
un)
                UnionOf -> ([SENTENCE] -> SENTENCE
mkBD [SENTENCE]
jl, Sign
un)
    DataComplementOf cdr :: DataRange
cdr -> do
        (dc :: SENTENCE
dc, sig :: Sign
sig) <- Sign -> DataRange -> VarOrIndi -> Result (SENTENCE, Sign)
mapDataRange Sign
cSig DataRange
cdr VarOrIndi
var
        (SENTENCE, Sign) -> Result (SENTENCE, Sign)
forall (m :: * -> *) a. Monad m => a -> m a
return (SENTENCE -> SENTENCE
mkBN SENTENCE
dc, Sign
sig)
    DataOneOf cs :: [Literal]
cs -> do
        [Either (SENTENCE, SENTENCE) TERM]
cl <- (Literal -> Result (Either (SENTENCE, SENTENCE) TERM))
-> [Literal] -> Result [Either (SENTENCE, SENTENCE) TERM]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (VarOrIndi -> Literal -> Result (Either (SENTENCE, SENTENCE) TERM)
mapLitAux VarOrIndi
var) [Literal]
cs
        let (sens :: [(SENTENCE, SENTENCE)]
sens, ts :: [TERM]
ts) = ([Either (SENTENCE, SENTENCE) TERM] -> [(SENTENCE, SENTENCE)]
forall a b. [Either a b] -> [a]
lefts [Either (SENTENCE, SENTENCE) TERM]
cl, [Either (SENTENCE, SENTENCE) TERM] -> [TERM]
forall a b. [Either a b] -> [b]
rights [Either (SENTENCE, SENTENCE) TERM]
cl)
            sl :: [SENTENCE]
sl = ((SENTENCE, SENTENCE) -> SENTENCE)
-> [(SENTENCE, SENTENCE)] -> [SENTENCE]
forall a b. (a -> b) -> [a] -> [b]
map (\ (s1 :: SENTENCE
s1, s2 :: SENTENCE
s2) -> [SENTENCE] -> SENTENCE
mkBC [SENTENCE
s1, SENTENCE
s2]) [(SENTENCE, SENTENCE)]
sens
        [SENTENCE]
tl <- (TERM -> Result SENTENCE) -> [TERM] -> Result [SENTENCE]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\ x :: TERM
x -> SENTENCE -> Result SENTENCE
forall (m :: * -> *) a. Monad m => a -> m a
return (SENTENCE -> Result SENTENCE) -> SENTENCE -> Result SENTENCE
forall a b. (a -> b) -> a -> b
$ ATOM -> SENTENCE
mkAtoms (ATOM -> SENTENCE) -> ATOM -> SENTENCE
forall a b. (a -> b) -> a -> b
$ TERM -> [TERM_SEQ] -> ATOM
Atom TERM
x [TERM -> TERM_SEQ
Term_seq TERM
uid]) [TERM]
ts
        (SENTENCE, Sign) -> Result (SENTENCE, Sign)
forall (m :: * -> *) a. Monad m => a -> m a
return ([SENTENCE] -> SENTENCE
mkBD ([SENTENCE] -> SENTENCE) -> [SENTENCE] -> SENTENCE
forall a b. (a -> b) -> a -> b
$ [SENTENCE]
tl [SENTENCE] -> [SENTENCE] -> [SENTENCE]
forall a. [a] -> [a] -> [a]
++ [SENTENCE]
sl, Sign
cSig)
    DataType dt :: IRI
dt rlst :: [(IRI, Literal)]
rlst -> do
        let sent :: SENTENCE
sent = Token -> [TERM] -> SENTENCE
mkTermAtoms (IRI -> Token
uriToTok IRI
dt) [TERM
uid]
        (sens :: [SENTENCE]
sens, sigL :: [Sign]
sigL) <- ((IRI, Literal) -> Result (SENTENCE, Sign))
-> [(IRI, Literal)] -> Result ([SENTENCE], [Sign])
forall (m :: * -> *) a b c.
Applicative m =>
(a -> m (b, c)) -> [a] -> m ([b], [c])
mapAndUnzipM (Sign -> Int -> TERM -> (IRI, Literal) -> Result (SENTENCE, Sign)
mapFacet Sign
cSig Int
i TERM
uid) [(IRI, Literal)]
rlst
        (SENTENCE, Sign) -> Result (SENTENCE, Sign)
forall (m :: * -> *) a. Monad m => a -> m a
return ([SENTENCE] -> SENTENCE
mkBC ([SENTENCE] -> SENTENCE) -> [SENTENCE] -> SENTENCE
forall a b. (a -> b) -> a -> b
$ SENTENCE
sent SENTENCE -> [SENTENCE] -> [SENTENCE]
forall a. a -> [a] -> [a]
: [SENTENCE]
sens, [Sign] -> Sign
uniteL ([Sign] -> Sign) -> [Sign] -> Sign
forall a b. (a -> b) -> a -> b
$ Sign
cSig Sign -> [Sign] -> [Sign]
forall a. a -> [a] -> [a]
: [Sign]
sigL)

-- | mapping of a tuple of ConstrainingFacet and RestictionValue
mapFacet :: Sign -> Int -> TERM -> (ConstrainingFacet, RestrictionValue)
    -> Result (SENTENCE, Sign)
mapFacet :: Sign -> Int -> TERM -> (IRI, Literal) -> Result (SENTENCE, Sign)
mapFacet sig :: Sign
sig v :: Int
v var :: TERM
var (f :: IRI
f, r :: Literal
r) = do
    Either (SENTENCE, SENTENCE) TERM
l <- Int -> Literal -> Result (Either (SENTENCE, SENTENCE) TERM)
mapLit Int
v Literal
r
    let sign :: Sign
sign = Sign -> Sign -> Sign
unite Sign
sig (Sign -> Sign) -> Sign -> Sign
forall a b. (a -> b) -> a -> b
$ Sign
emptySig {
                  discourseNames :: Set Id
discourseNames = [Id] -> Set Id
forall a. Ord a => [a] -> Set a
Set.fromList [String -> Id
stringToId (String -> Id) -> String -> Id
forall a b. (a -> b) -> a -> b
$ IRI -> String
showIRI
                                                  (IRI -> String) -> IRI -> String
forall a b. (a -> b) -> a -> b
$ IRI -> IRI
stripReservedPrefix IRI
f]}
    case Either (SENTENCE, SENTENCE) TERM
l of
        Right lit :: TERM
lit -> (SENTENCE, Sign) -> Result (SENTENCE, Sign)
forall (m :: * -> *) a. Monad m => a -> m a
return (Token -> [TERM] -> SENTENCE
mkTermAtoms (IRI -> Token
uriToTok IRI
f) [TERM
lit, TERM
var], Sign
sign)
        Left (s1 :: SENTENCE
s1, s2 :: SENTENCE
s2) -> (SENTENCE, Sign) -> Result (SENTENCE, Sign)
forall (m :: * -> *) a. Monad m => a -> m a
return ([SENTENCE] -> SENTENCE
mkBC [Token -> [TERM] -> SENTENCE
mkTermAtoms (IRI -> Token
uriToTok IRI
f)
                    [VarOrIndi -> TERM
mkVTerm (VarOrIndi -> TERM) -> VarOrIndi -> TERM
forall a b. (a -> b) -> a -> b
$ Int -> VarOrIndi
OVar Int
v, TERM
var], SENTENCE
s1, SENTENCE
s2], Sign
sign)

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

mapCard :: Bool -> Sign -> CardinalityType -> Int
    -> Either ObjectPropertyExpression DataPropertyExpression
    -> Maybe (Either ClassExpression DataRange) -> Int
    -> Result (SENTENCE, Sign)
mapCard :: Bool
-> Sign
-> CardinalityType
-> Int
-> Either ObjectPropertyExpression IRI
-> Maybe (Either ClassExpression DataRange)
-> Int
-> Result (SENTENCE, Sign)
mapCard b :: Bool
b cSig :: Sign
cSig 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]
        vLst :: [VarOrIndi]
vLst = (Int -> VarOrIndi) -> [Int] -> [VarOrIndi]
forall a b. (a -> b) -> [a] -> [b]
map Int -> VarOrIndi
OVar [Int]
vlst
        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]
        vLstM :: [VarOrIndi]
vLstM = (Int -> VarOrIndi) -> [Int] -> [VarOrIndi]
forall a b. (a -> b) -> [a] -> [b]
map Int -> VarOrIndi
OVar [Int]
vlstM
    (dOut :: [SENTENCE]
dOut, sigL :: [Sign]
sigL) <- case Maybe (Either ClassExpression DataRange)
d of
        Nothing -> ([SENTENCE], [Sign]) -> Result ([SENTENCE], [Sign])
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 ((VarOrIndi, Int) -> Result (SENTENCE, Sign))
-> [(VarOrIndi, Int)] -> Result ([SENTENCE], [Sign])
forall (m :: * -> *) a b c.
Applicative m =>
(a -> m (b, c)) -> [a] -> m ([b], [c])
mapAndUnzipM
                        ((VarOrIndi -> Int -> Result (SENTENCE, Sign))
-> (VarOrIndi, Int) -> Result (SENTENCE, Sign)
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry ((VarOrIndi -> Int -> Result (SENTENCE, Sign))
 -> (VarOrIndi, Int) -> Result (SENTENCE, Sign))
-> (VarOrIndi -> Int -> Result (SENTENCE, Sign))
-> (VarOrIndi, Int)
-> Result (SENTENCE, Sign)
forall a b. (a -> b) -> a -> b
$ Sign
-> ClassExpression -> VarOrIndi -> Int -> Result (SENTENCE, Sign)
mapDescription Sign
cSig ClassExpression
ce) ([(VarOrIndi, Int)] -> Result ([SENTENCE], [Sign]))
-> [(VarOrIndi, Int)] -> Result ([SENTENCE], [Sign])
forall a b. (a -> b) -> a -> b
$ [VarOrIndi] -> [Int] -> [(VarOrIndi, Int)]
forall t t1. [t] -> [t1] -> [(t, t1)]
zip [VarOrIndi]
vLst [Int]
vlst
           else let Right dr :: DataRange
dr = Either ClassExpression DataRange
y in (VarOrIndi -> Result (SENTENCE, Sign))
-> [VarOrIndi] -> Result ([SENTENCE], [Sign])
forall (m :: * -> *) a b c.
Applicative m =>
(a -> m (b, c)) -> [a] -> m ([b], [c])
mapAndUnzipM (Sign -> DataRange -> VarOrIndi -> Result (SENTENCE, Sign)
mapDataRange Sign
cSig DataRange
dr) [VarOrIndi]
vLst
    let dlst :: [SENTENCE]
dlst = ((Int, Int) -> SENTENCE) -> [(Int, Int)] -> [SENTENCE]
forall a b. (a -> b) -> [a] -> [b]
map (\ (x :: Int
x, y :: Int
y) -> SENTENCE -> SENTENCE
mkBN (SENTENCE -> SENTENCE) -> SENTENCE -> SENTENCE
forall a b. (a -> b) -> a -> b
$ TERM -> TERM -> SENTENCE
mkAE (Int -> TERM
mkNTERM Int
x) (TERM -> SENTENCE) -> TERM -> SENTENCE
forall a b. (a -> b) -> a -> b
$ Int -> TERM
mkNTERM Int
y)
                        ([(Int, Int)] -> [SENTENCE]) -> [(Int, Int)] -> [SENTENCE]
forall a b. (a -> b) -> a -> b
$ [Int] -> [Int] -> [(Int, Int)]
forall t t1. [t] -> [t1] -> [(t, t1)]
comPairs [Int]
vlst [Int]
vlst
        dlstM :: [SENTENCE]
dlstM = ((Int, Int) -> SENTENCE) -> [(Int, Int)] -> [SENTENCE]
forall a b. (a -> b) -> [a] -> [b]
map (\ (x :: Int
x, y :: Int
y) -> TERM -> TERM -> SENTENCE
mkAE (Int -> TERM
mkNTERM Int
x) (TERM -> SENTENCE) -> TERM -> SENTENCE
forall a b. (a -> b) -> a -> b
$ Int -> TERM
mkNTERM Int
y)
                        ([(Int, Int)] -> [SENTENCE]) -> [(Int, Int)] -> [SENTENCE]
forall a b. (a -> b) -> a -> b
$ [Int] -> [Int] -> [(Int, Int)]
forall t t1. [t] -> [t1] -> [(t, t1)]
comPairs [Int]
vlstM [Int]
vlstM
        qVars :: [NAME_OR_SEQMARK]
qVars = (Int -> NAME_OR_SEQMARK) -> [Int] -> [NAME_OR_SEQMARK]
forall a b. (a -> b) -> [a] -> [b]
map Int -> NAME_OR_SEQMARK
mkNAME [Int]
vlst
        qVarsM :: [NAME_OR_SEQMARK]
qVarsM = (Int -> NAME_OR_SEQMARK) -> [Int] -> [NAME_OR_SEQMARK]
forall a b. (a -> b) -> [a] -> [b]
map Int -> NAME_OR_SEQMARK
mkNAME [Int]
vlstM
    [SENTENCE]
oProps <- Bool
-> Sign
-> Either ObjectPropertyExpression IRI
-> Int
-> [VarOrIndi]
-> Result [SENTENCE]
cardProps Bool
b Sign
cSig Either ObjectPropertyExpression IRI
prop Int
var [VarOrIndi]
vLst
    [SENTENCE]
oPropsM <- Bool
-> Sign
-> Either ObjectPropertyExpression IRI
-> Int
-> [VarOrIndi]
-> Result [SENTENCE]
cardProps Bool
b Sign
cSig Either ObjectPropertyExpression IRI
prop Int
var [VarOrIndi]
vLstM
    let minLst :: SENTENCE
minLst = [NAME_OR_SEQMARK] -> SENTENCE -> SENTENCE
mkQE [NAME_OR_SEQMARK]
qVars (SENTENCE -> SENTENCE) -> SENTENCE -> SENTENCE
forall a b. (a -> b) -> a -> b
$ [SENTENCE] -> SENTENCE
mkBC ([SENTENCE] -> SENTENCE) -> [SENTENCE] -> SENTENCE
forall a b. (a -> b) -> a -> b
$ [SENTENCE]
dlst [SENTENCE] -> [SENTENCE] -> [SENTENCE]
forall a. [a] -> [a] -> [a]
++ [SENTENCE]
dOut [SENTENCE] -> [SENTENCE] -> [SENTENCE]
forall a. [a] -> [a] -> [a]
++ [SENTENCE]
oProps
        maxLst :: SENTENCE
maxLst = [NAME_OR_SEQMARK] -> SENTENCE -> SENTENCE
mkQE [NAME_OR_SEQMARK]
qVarsM (SENTENCE -> SENTENCE) -> SENTENCE -> SENTENCE
forall a b. (a -> b) -> a -> b
$ SENTENCE -> SENTENCE -> SENTENCE
mkBI ([SENTENCE] -> SENTENCE
mkBC ([SENTENCE] -> SENTENCE) -> [SENTENCE] -> SENTENCE
forall a b. (a -> b) -> a -> b
$ [SENTENCE]
oPropsM [SENTENCE] -> [SENTENCE] -> [SENTENCE]
forall a. [a] -> [a] -> [a]
++ [SENTENCE]
dOut) (SENTENCE -> SENTENCE) -> SENTENCE -> SENTENCE
forall a b. (a -> b) -> a -> b
$ [SENTENCE] -> SENTENCE
mkBD [SENTENCE]
dlstM
    (SENTENCE, Sign) -> Result (SENTENCE, Sign)
forall (m :: * -> *) a. Monad m => a -> m a
return ((SENTENCE, Sign) -> Result (SENTENCE, Sign))
-> (SENTENCE, Sign) -> Result (SENTENCE, Sign)
forall a b. (a -> b) -> a -> b
$ case CardinalityType
ct of
                MinCardinality -> (SENTENCE
minLst, Sign
cSig)
                MaxCardinality -> (SENTENCE
maxLst, Sign
cSig)
                ExactCardinality -> ([SENTENCE] -> SENTENCE
mkBC [SENTENCE
minLst, SENTENCE
maxLst], [Sign] -> Sign
uniteL [Sign]
sigL)

-- | mapping of OWL Descriptions
mapDescription :: Sign -> ClassExpression -> VarOrIndi -> Int
               -> Result (SENTENCE, Sign)
mapDescription :: Sign
-> ClassExpression -> VarOrIndi -> Int -> Result (SENTENCE, Sign)
mapDescription cSig :: Sign
cSig des :: ClassExpression
des oVar :: VarOrIndi
oVar aVar :: Int
aVar =
  let varN :: Token
varN = case VarOrIndi
oVar of
        OVar v :: Int
v -> Int -> Token
mkNName Int
v
        OIndi i :: IRI
i -> IRI -> Token
uriToTok IRI
i
      var :: Int
var = case VarOrIndi
oVar of
        OVar v :: Int
v -> Int
v
        OIndi _ -> Int
aVar
  in case ClassExpression
des of
    Expression cl :: IRI
cl -> do
        SENTENCE
ne <- Sign -> IRI -> Token -> Result SENTENCE
mapClassIRI Sign
cSig IRI
cl Token
varN
        (SENTENCE, Sign) -> Result (SENTENCE, Sign)
forall (m :: * -> *) a. Monad m => a -> m a
return (SENTENCE
ne, Sign
cSig)
    ObjectJunction jt :: JunctionType
jt desL :: [ClassExpression]
desL -> do
        (cel :: [SENTENCE]
cel, dSig :: [Sign]
dSig) <- (ClassExpression -> Result (SENTENCE, Sign))
-> [ClassExpression] -> Result ([SENTENCE], [Sign])
forall (m :: * -> *) a b c.
Applicative m =>
(a -> m (b, c)) -> [a] -> m ([b], [c])
mapAndUnzipM ((\ w :: Sign
w x :: VarOrIndi
x y :: Int
y z :: ClassExpression
z -> Sign
-> ClassExpression -> VarOrIndi -> Int -> Result (SENTENCE, Sign)
mapDescription Sign
w ClassExpression
z VarOrIndi
x Int
y)
                            Sign
cSig VarOrIndi
oVar Int
aVar) [ClassExpression]
desL
        let un :: Sign
un = [Sign] -> Sign
uniteL [Sign]
dSig
        (SENTENCE, Sign) -> Result (SENTENCE, Sign)
forall (m :: * -> *) a. Monad m => a -> m a
return ((SENTENCE, Sign) -> Result (SENTENCE, Sign))
-> (SENTENCE, Sign) -> Result (SENTENCE, Sign)
forall a b. (a -> b) -> a -> b
$ case JunctionType
jt of
                UnionOf -> ([SENTENCE] -> SENTENCE
mkBD [SENTENCE]
cel, Sign
un)
                IntersectionOf -> ([SENTENCE] -> SENTENCE
mkBC [SENTENCE]
cel, Sign
un)
    ObjectComplementOf descr :: ClassExpression
descr -> do
        (ce :: SENTENCE
ce, dSig :: Sign
dSig) <- Sign
-> ClassExpression -> VarOrIndi -> Int -> Result (SENTENCE, Sign)
mapDescription Sign
cSig ClassExpression
descr VarOrIndi
oVar Int
aVar
        (SENTENCE, Sign) -> Result (SENTENCE, Sign)
forall (m :: * -> *) a. Monad m => a -> m a
return (SENTENCE -> SENTENCE
mkBN SENTENCE
ce, Sign
dSig)
    ObjectOneOf il :: [IRI]
il -> do
        [TERM]
nil <- (IRI -> Result TERM) -> [IRI] -> Result [TERM]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Sign -> IRI -> Result TERM
mapIndivIRI Sign
cSig) [IRI]
il
        (SENTENCE, Sign) -> Result (SENTENCE, Sign)
forall (m :: * -> *) a. Monad m => a -> m a
return ([SENTENCE] -> SENTENCE
mkBD ([SENTENCE] -> SENTENCE) -> [SENTENCE] -> SENTENCE
forall a b. (a -> b) -> a -> b
$ (TERM -> SENTENCE) -> [TERM] -> [SENTENCE]
forall a b. (a -> b) -> [a] -> [b]
map (TERM -> TERM -> SENTENCE
mkAE (TERM -> TERM -> SENTENCE) -> TERM -> TERM -> SENTENCE
forall a b. (a -> b) -> a -> b
$ Token -> TERM
Name_term Token
varN) [TERM]
nil, Sign
cSig)
    ObjectValuesFrom qt :: QuantifierType
qt oprop :: ObjectPropertyExpression
oprop descr :: ClassExpression
descr -> let v :: Int
v = Int
var Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1 in do
        SENTENCE
ope <- Sign -> ObjectPropertyExpression -> Int -> Int -> Result SENTENCE
mapOPE Sign
cSig ObjectPropertyExpression
oprop Int
var Int
v
        (ce :: SENTENCE
ce, dSig :: Sign
dSig) <- Sign
-> ClassExpression -> VarOrIndi -> Int -> Result (SENTENCE, Sign)
mapDescription Sign
cSig ClassExpression
descr (Int -> VarOrIndi
OVar Int
v) (Int -> Result (SENTENCE, Sign)) -> Int -> Result (SENTENCE, Sign)
forall a b. (a -> b) -> a -> b
$ Int
aVar Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1
        (SENTENCE, Sign) -> Result (SENTENCE, Sign)
forall (m :: * -> *) a. Monad m => a -> m a
return ((SENTENCE, Sign) -> Result (SENTENCE, Sign))
-> (SENTENCE, Sign) -> Result (SENTENCE, Sign)
forall a b. (a -> b) -> a -> b
$ case QuantifierType
qt of
            SomeValuesFrom -> ([NAME_OR_SEQMARK] -> SENTENCE -> SENTENCE
mkQE [Int -> NAME_OR_SEQMARK
mkNAME Int
v] (SENTENCE -> SENTENCE) -> SENTENCE -> SENTENCE
forall a b. (a -> b) -> a -> b
$ [SENTENCE] -> SENTENCE
mkBC [SENTENCE
ope, SENTENCE
ce], Sign
dSig)
            AllValuesFrom -> ([NAME_OR_SEQMARK] -> SENTENCE -> SENTENCE
mkQU [Int -> NAME_OR_SEQMARK
mkNAME Int
v] (SENTENCE -> SENTENCE) -> SENTENCE -> SENTENCE
forall a b. (a -> b) -> a -> b
$ SENTENCE -> SENTENCE -> SENTENCE
mkBI SENTENCE
ope SENTENCE
ce, Sign
dSig)
    ObjectHasSelf oprop :: ObjectPropertyExpression
oprop -> (Sign
 -> ObjectPropertyExpression
 -> VarOrIndi
 -> VarOrIndi
 -> Result SENTENCE)
-> Sign
-> ObjectPropertyExpression
-> VarOrIndi
-> VarOrIndi
-> Result (SENTENCE, Sign)
forall (m :: * -> *) t4 t t1 t2 t3.
Monad m =>
(t4 -> t -> t1 -> t2 -> m t3) -> t4 -> t -> t1 -> t2 -> m (t3, t4)
smap Sign
-> ObjectPropertyExpression
-> VarOrIndi
-> VarOrIndi
-> Result SENTENCE
mapObjProp Sign
cSig ObjectPropertyExpression
oprop VarOrIndi
oVar VarOrIndi
oVar
    ObjectHasValue oprop :: ObjectPropertyExpression
oprop indiv :: IRI
indiv -> (Sign
 -> ObjectPropertyExpression
 -> VarOrIndi
 -> VarOrIndi
 -> Result SENTENCE)
-> Sign
-> ObjectPropertyExpression
-> VarOrIndi
-> VarOrIndi
-> Result (SENTENCE, Sign)
forall (m :: * -> *) t4 t t1 t2 t3.
Monad m =>
(t4 -> t -> t1 -> t2 -> m t3) -> t4 -> t -> t1 -> t2 -> m (t3, t4)
smap Sign
-> ObjectPropertyExpression
-> VarOrIndi
-> VarOrIndi
-> Result SENTENCE
mapObjProp Sign
cSig ObjectPropertyExpression
oprop VarOrIndi
oVar (IRI -> VarOrIndi
OIndi IRI
indiv)
    ObjectCardinality (Cardinality ct :: CardinalityType
ct n :: Int
n oprop :: ObjectPropertyExpression
oprop d :: Maybe ClassExpression
d) -> Bool
-> Sign
-> CardinalityType
-> Int
-> Either ObjectPropertyExpression IRI
-> Maybe (Either ClassExpression DataRange)
-> Int
-> Result (SENTENCE, Sign)
mapCard Bool
True Sign
cSig 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 qt :: QuantifierType
qt dpe :: [IRI]
dpe dr :: DataRange
dr -> let varNN :: Token
varNN = Int -> Token
mkNName (Int -> Token) -> Int -> Token
forall a b. (a -> b) -> a -> b
$ Int
var Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1 in do
        (drSent :: SENTENCE
drSent, drSig :: Sign
drSig) <- Sign -> DataRange -> VarOrIndi -> Result (SENTENCE, Sign)
mapDataRange Sign
cSig DataRange
dr (VarOrIndi -> Result (SENTENCE, Sign))
-> VarOrIndi -> Result (SENTENCE, Sign)
forall a b. (a -> b) -> a -> b
$ Int -> VarOrIndi
OVar (Int -> VarOrIndi) -> Int -> VarOrIndi
forall a b. (a -> b) -> a -> b
$ Int
var Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1
        [SENTENCE]
senl <- (IRI -> Result SENTENCE) -> [IRI] -> Result [SENTENCE]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Sign -> VarOrIndi -> VarOrIndi -> IRI -> Result SENTENCE
mapDataPropI Sign
cSig (Int -> VarOrIndi
OVar Int
var) (VarOrIndi -> IRI -> Result SENTENCE)
-> VarOrIndi -> IRI -> Result SENTENCE
forall a b. (a -> b) -> a -> b
$ Int -> VarOrIndi
OVar (Int -> VarOrIndi) -> Int -> VarOrIndi
forall a b. (a -> b) -> a -> b
$ Int
var Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1) [IRI]
dpe
        let sent :: SENTENCE
sent = [SENTENCE] -> SENTENCE
mkBC ([SENTENCE] -> SENTENCE) -> [SENTENCE] -> SENTENCE
forall a b. (a -> b) -> a -> b
$ SENTENCE
drSent SENTENCE -> [SENTENCE] -> [SENTENCE]
forall a. a -> [a] -> [a]
: [SENTENCE]
senl
        (SENTENCE, Sign) -> Result (SENTENCE, Sign)
forall (m :: * -> *) a. Monad m => a -> m a
return ((SENTENCE, Sign) -> Result (SENTENCE, Sign))
-> (SENTENCE, Sign) -> Result (SENTENCE, Sign)
forall a b. (a -> b) -> a -> b
$ case QuantifierType
qt of
            AllValuesFrom -> ([NAME_OR_SEQMARK] -> SENTENCE -> SENTENCE
mkQU [Token -> NAME_OR_SEQMARK
Name Token
varNN] SENTENCE
sent, Sign
drSig)
            SomeValuesFrom -> ([NAME_OR_SEQMARK] -> SENTENCE -> SENTENCE
mkQE [Token -> NAME_OR_SEQMARK
Name Token
varNN] SENTENCE
sent, Sign
drSig)
    DataHasValue dpe :: IRI
dpe c :: Literal
c -> do
        let nvar :: Int
nvar = Int
var Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1
        Either (SENTENCE, SENTENCE) TERM
con <- Int -> Literal -> Result (Either (SENTENCE, SENTENCE) TERM)
mapLit Int
nvar Literal
c
        case Either (SENTENCE, SENTENCE) TERM
con of
            Right lit :: TERM
lit -> (SENTENCE, Sign) -> Result (SENTENCE, Sign)
forall (m :: * -> *) a. Monad m => a -> m a
return (ATOM -> SENTENCE
mkAtoms (ATOM -> SENTENCE) -> ATOM -> SENTENCE
forall a b. (a -> b) -> a -> b
$ TERM -> [TERM_SEQ] -> ATOM
Atom (Token -> TERM
Name_term (Token -> TERM) -> Token -> TERM
forall a b. (a -> b) -> a -> b
$ IRI -> Token
uriToTok IRI
dpe)
                    [Token -> TERM_SEQ
mkTermSeq Token
varN, TERM -> TERM_SEQ
Term_seq TERM
lit], Sign
cSig)
            Left (s1 :: SENTENCE
s1, s2 :: SENTENCE
s2) -> do
                SENTENCE
sens <- Sign -> IRI -> VarOrIndi -> VarOrIndi -> Result SENTENCE
mapDataProp Sign
cSig IRI
dpe VarOrIndi
oVar (VarOrIndi -> Result SENTENCE) -> VarOrIndi -> Result SENTENCE
forall a b. (a -> b) -> a -> b
$ Int -> VarOrIndi
OVar Int
nvar
                (SENTENCE, Sign) -> Result (SENTENCE, Sign)
forall (m :: * -> *) a. Monad m => a -> m a
return ([SENTENCE] -> SENTENCE
mkBC [SENTENCE
sens, SENTENCE
s1, SENTENCE
s2], Sign
cSig)
    DataCardinality (Cardinality ct :: CardinalityType
ct n :: Int
n dpe :: IRI
dpe dr :: Maybe DataRange
dr) -> Bool
-> Sign
-> CardinalityType
-> Int
-> Either ObjectPropertyExpression IRI
-> Maybe (Either ClassExpression DataRange)
-> Int
-> Result (SENTENCE, Sign)
mapCard Bool
False Sign
cSig 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 :: Sign -> Int -> [ClassExpression]
    -> Result ([SENTENCE], Sign)
mapDescriptionList :: Sign -> Int -> [ClassExpression] -> Result ([SENTENCE], Sign)
mapDescriptionList cSig :: Sign
cSig n :: Int
n lst :: [ClassExpression]
lst = do
    (sens :: [SENTENCE]
sens, lSig :: [Sign]
lSig) <- (ClassExpression -> Result (SENTENCE, Sign))
-> [ClassExpression] -> Result ([SENTENCE], [Sign])
forall (m :: * -> *) a b c.
Applicative m =>
(a -> m (b, c)) -> [a] -> m ([b], [c])
mapAndUnzipM ((\ w :: Sign
w x :: VarOrIndi
x y :: Int
y z :: ClassExpression
z ->
                       Sign
-> ClassExpression -> VarOrIndi -> Int -> Result (SENTENCE, Sign)
mapDescription Sign
w ClassExpression
z VarOrIndi
x Int
y) Sign
cSig (Int -> VarOrIndi
OVar Int
n) Int
n) [ClassExpression]
lst
    Sign
sig <- [Sign] -> Result Sign
sigUnionL [Sign]
lSig
    ([SENTENCE], Sign) -> Result ([SENTENCE], Sign)
forall (m :: * -> *) a. Monad m => a -> m a
return ([SENTENCE]
sens, Sign
sig)

-- | Mapping of a list of pairs of descriptions
mapDescriptionListP :: Sign -> Int -> [(ClassExpression, ClassExpression)]
    -> Result ([(SENTENCE, SENTENCE)], Sign)
mapDescriptionListP :: Sign
-> Int
-> [(ClassExpression, ClassExpression)]
-> Result ([(SENTENCE, SENTENCE)], Sign)
mapDescriptionListP cSig :: Sign
cSig 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
    (llst :: [SENTENCE]
llst, ssSig :: Sign
ssSig) <- Sign -> Int -> [ClassExpression] -> Result ([SENTENCE], Sign)
mapDescriptionList Sign
cSig Int
n [ClassExpression]
l
    (rlst :: [SENTENCE]
rlst, tSig :: Sign
tSig) <- Sign -> Int -> [ClassExpression] -> Result ([SENTENCE], Sign)
mapDescriptionList Sign
cSig Int
n [ClassExpression]
r
    ([(SENTENCE, SENTENCE)], Sign)
-> Result ([(SENTENCE, SENTENCE)], Sign)
forall (m :: * -> *) a. Monad m => a -> m a
return ([SENTENCE] -> [SENTENCE] -> [(SENTENCE, SENTENCE)]
forall t t1. [t] -> [t1] -> [(t, t1)]
zip [SENTENCE]
llst [SENTENCE]
rlst, Sign -> Sign -> Sign
unite Sign
ssSig Sign
tSig)

mapClassAssertion :: TERM -> (ClassExpression, SENTENCE) -> TEXT
mapClassAssertion :: TERM -> (ClassExpression, SENTENCE) -> TEXT
mapClassAssertion ind :: TERM
ind (ce :: ClassExpression
ce, sent :: SENTENCE
sent) = case ClassExpression
ce of
    Expression _ -> SENTENCE -> TEXT
senToText SENTENCE
sent
    _ -> SENTENCE -> TEXT
senToText (SENTENCE -> TEXT) -> SENTENCE -> TEXT
forall a b. (a -> b) -> a -> b
$ (SENTENCE -> SENTENCE
mk1QU (SENTENCE -> SENTENCE)
-> (SENTENCE -> SENTENCE) -> SENTENCE -> SENTENCE
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SENTENCE -> SENTENCE -> SENTENCE
mkBI (TERM -> TERM -> SENTENCE
mkAE TERM
mk1NTERM TERM
ind)) SENTENCE
sent

mapCharact :: Sign -> ObjectPropertyExpression -> Character -> Result TEXT
mapCharact :: Sign -> ObjectPropertyExpression -> Character -> Result TEXT
mapCharact cSig :: Sign
cSig ope :: ObjectPropertyExpression
ope c :: Character
c = case Character
c of
    Functional -> do
        SENTENCE
so1 <- Sign -> ObjectPropertyExpression -> Int -> Int -> Result SENTENCE
mapOPE Sign
cSig ObjectPropertyExpression
ope 1 2
        SENTENCE
so2 <- Sign -> ObjectPropertyExpression -> Int -> Int -> Result SENTENCE
mapOPE Sign
cSig ObjectPropertyExpression
ope 1 3
        TEXT -> Result TEXT
forall (m :: * -> *) a. Monad m => a -> m a
return (TEXT -> Result TEXT) -> TEXT -> Result TEXT
forall a b. (a -> b) -> a -> b
$ [NAME_OR_SEQMARK] -> [SENTENCE] -> TERM -> TERM -> TEXT
mkQUBI ((Int -> NAME_OR_SEQMARK) -> [Int] -> [NAME_OR_SEQMARK]
forall a b. (a -> b) -> [a] -> [b]
map Int -> NAME_OR_SEQMARK
mkNAME [1, 2, 3]) [SENTENCE
so1, SENTENCE
so2]
                (Int -> TERM
mkNTERM 2) (Int -> TERM
mkNTERM 3)
    InverseFunctional -> do
        SENTENCE
so1 <- Sign -> ObjectPropertyExpression -> Int -> Int -> Result SENTENCE
mapOPE Sign
cSig ObjectPropertyExpression
ope 1 3
        SENTENCE
so2 <- Sign -> ObjectPropertyExpression -> Int -> Int -> Result SENTENCE
mapOPE Sign
cSig ObjectPropertyExpression
ope 2 3
        TEXT -> Result TEXT
forall (m :: * -> *) a. Monad m => a -> m a
return (TEXT -> Result TEXT) -> TEXT -> Result TEXT
forall a b. (a -> b) -> a -> b
$ [NAME_OR_SEQMARK] -> [SENTENCE] -> TERM -> TERM -> TEXT
mkQUBI ((Int -> NAME_OR_SEQMARK) -> [Int] -> [NAME_OR_SEQMARK]
forall a b. (a -> b) -> [a] -> [b]
map Int -> NAME_OR_SEQMARK
mkNAME [1, 2, 3]) [SENTENCE
so1, SENTENCE
so2]
                (Int -> TERM
mkNTERM 1) (Int -> TERM
mkNTERM 2)
    Reflexive -> do
        SENTENCE
so <- Sign -> ObjectPropertyExpression -> Int -> Int -> Result SENTENCE
mapOPE Sign
cSig ObjectPropertyExpression
ope 1 1
        TEXT -> Result TEXT
forall (m :: * -> *) a. Monad m => a -> m a
return (TEXT -> Result TEXT) -> TEXT -> Result TEXT
forall a b. (a -> b) -> a -> b
$ SENTENCE -> TEXT
senToText (SENTENCE -> TEXT) -> SENTENCE -> TEXT
forall a b. (a -> b) -> a -> b
$ SENTENCE -> SENTENCE
mk1QU SENTENCE
so
    Irreflexive -> do
        SENTENCE
so <- Sign -> ObjectPropertyExpression -> Int -> Int -> Result SENTENCE
mapOPE Sign
cSig ObjectPropertyExpression
ope 1 1
        TEXT -> Result TEXT
forall (m :: * -> *) a. Monad m => a -> m a
return (TEXT -> Result TEXT) -> TEXT -> Result TEXT
forall a b. (a -> b) -> a -> b
$ SENTENCE -> TEXT
senToText (SENTENCE -> TEXT) -> SENTENCE -> TEXT
forall a b. (a -> b) -> a -> b
$ SENTENCE -> SENTENCE
mk1QU (SENTENCE -> SENTENCE) -> SENTENCE -> SENTENCE
forall a b. (a -> b) -> a -> b
$ SENTENCE -> SENTENCE
mkBN SENTENCE
so
    Symmetric -> do
        SENTENCE
so1 <- Sign -> ObjectPropertyExpression -> Int -> Int -> Result SENTENCE
mapOPE Sign
cSig ObjectPropertyExpression
ope 1 2
        SENTENCE
so2 <- Sign -> ObjectPropertyExpression -> Int -> Int -> Result SENTENCE
mapOPE Sign
cSig ObjectPropertyExpression
ope 2 1
        TEXT -> Result TEXT
forall (m :: * -> *) a. Monad m => a -> m a
return (TEXT -> Result TEXT) -> TEXT -> Result TEXT
forall a b. (a -> b) -> a -> b
$ SENTENCE -> TEXT
senToText (SENTENCE -> TEXT) -> SENTENCE -> TEXT
forall a b. (a -> b) -> a -> b
$ [NAME_OR_SEQMARK] -> SENTENCE -> SENTENCE
mkQU [Int -> NAME_OR_SEQMARK
mkNAME 1, Int -> NAME_OR_SEQMARK
mkNAME 2] (SENTENCE -> SENTENCE) -> SENTENCE -> SENTENCE
forall a b. (a -> b) -> a -> b
$ SENTENCE -> SENTENCE -> SENTENCE
mkBI SENTENCE
so1 SENTENCE
so2
    Asymmetric -> do
        SENTENCE
so1 <- Sign -> ObjectPropertyExpression -> Int -> Int -> Result SENTENCE
mapOPE Sign
cSig ObjectPropertyExpression
ope 1 2
        SENTENCE
so2 <- Sign -> ObjectPropertyExpression -> Int -> Int -> Result SENTENCE
mapOPE Sign
cSig ObjectPropertyExpression
ope 2 1
        TEXT -> Result TEXT
forall (m :: * -> *) a. Monad m => a -> m a
return (TEXT -> Result TEXT) -> TEXT -> Result TEXT
forall a b. (a -> b) -> a -> b
$ SENTENCE -> TEXT
senToText (SENTENCE -> TEXT) -> SENTENCE -> TEXT
forall a b. (a -> b) -> a -> b
$ [NAME_OR_SEQMARK] -> SENTENCE -> SENTENCE
mkQU [Int -> NAME_OR_SEQMARK
mkNAME 1, Int -> NAME_OR_SEQMARK
mkNAME 2] (SENTENCE -> SENTENCE) -> SENTENCE -> SENTENCE
forall a b. (a -> b) -> a -> b
$ SENTENCE -> SENTENCE -> SENTENCE
mkBI SENTENCE
so1 (SENTENCE -> SENTENCE) -> SENTENCE -> SENTENCE
forall a b. (a -> b) -> a -> b
$ SENTENCE -> SENTENCE
mkBN SENTENCE
so2
    Antisymmetric -> do
        SENTENCE
so1 <- Sign -> ObjectPropertyExpression -> Int -> Int -> Result SENTENCE
mapOPE Sign
cSig ObjectPropertyExpression
ope 1 2
        SENTENCE
so2 <- Sign -> ObjectPropertyExpression -> Int -> Int -> Result SENTENCE
mapOPE Sign
cSig ObjectPropertyExpression
ope 2 1
        TEXT -> Result TEXT
forall (m :: * -> *) a. Monad m => a -> m a
return (TEXT -> Result TEXT) -> TEXT -> Result TEXT
forall a b. (a -> b) -> a -> b
$ [NAME_OR_SEQMARK] -> [SENTENCE] -> TERM -> TERM -> TEXT
mkQUBI [Int -> NAME_OR_SEQMARK
mkNAME 1, Int -> NAME_OR_SEQMARK
mkNAME 2] [SENTENCE
so1, SENTENCE
so2] (Int -> TERM
mkNTERM 1) (Int -> TERM
mkNTERM 2)
    Transitive -> do
        SENTENCE
so1 <- Sign -> ObjectPropertyExpression -> Int -> Int -> Result SENTENCE
mapOPE Sign
cSig ObjectPropertyExpression
ope 1 2
        SENTENCE
so2 <- Sign -> ObjectPropertyExpression -> Int -> Int -> Result SENTENCE
mapOPE Sign
cSig ObjectPropertyExpression
ope 2 3
        SENTENCE
so3 <- Sign -> ObjectPropertyExpression -> Int -> Int -> Result SENTENCE
mapOPE Sign
cSig ObjectPropertyExpression
ope 1 3
        TEXT -> Result TEXT
forall (m :: * -> *) a. Monad m => a -> m a
return (TEXT -> Result TEXT) -> TEXT -> Result TEXT
forall a b. (a -> b) -> a -> b
$ SENTENCE -> TEXT
senToText (SENTENCE -> TEXT) -> SENTENCE -> TEXT
forall a b. (a -> b) -> a -> b
$ [NAME_OR_SEQMARK] -> SENTENCE -> SENTENCE
mkQU [Int -> NAME_OR_SEQMARK
mkNAME 1, Int -> NAME_OR_SEQMARK
mkNAME 2, Int -> NAME_OR_SEQMARK
mkNAME 3] (SENTENCE -> SENTENCE) -> SENTENCE -> SENTENCE
forall a b. (a -> b) -> a -> b
$ SENTENCE -> SENTENCE -> SENTENCE
mkBI
                ([SENTENCE] -> SENTENCE
mkBC [SENTENCE
so1, SENTENCE
so2]) SENTENCE
so3

mapKey :: Sign -> ClassExpression -> ([SENTENCE], [SENTENCE]) -> Int -> [Int]
    -> Result SENTENCE
mapKey :: Sign
-> ClassExpression
-> ([SENTENCE], [SENTENCE])
-> Int
-> [Int]
-> Result SENTENCE
mapKey cSig :: Sign
cSig ce :: ClassExpression
ce (pl :: [SENTENCE]
pl, npl :: [SENTENCE]
npl) p :: Int
p i :: [Int]
i = do
    (nce :: SENTENCE
nce, _) <- Sign
-> ClassExpression -> VarOrIndi -> Int -> Result (SENTENCE, Sign)
mapDescription Sign
cSig ClassExpression
ce (Int -> VarOrIndi
OVar 1) 1
    (c3 :: SENTENCE
c3, _) <- Sign
-> ClassExpression -> VarOrIndi -> Int -> Result (SENTENCE, Sign)
mapDescription Sign
cSig ClassExpression
ce (Int -> VarOrIndi
OVar Int
p) Int
p
    let un :: SENTENCE
un = [NAME_OR_SEQMARK] -> SENTENCE -> SENTENCE
mkQU [Int -> NAME_OR_SEQMARK
mkNAME Int
p] (SENTENCE -> SENTENCE) -> SENTENCE -> SENTENCE
forall a b. (a -> b) -> a -> b
$ SENTENCE -> SENTENCE -> SENTENCE
mkBI ([SENTENCE] -> SENTENCE
mkBC ([SENTENCE] -> SENTENCE) -> [SENTENCE] -> SENTENCE
forall a b. (a -> b) -> a -> b
$ SENTENCE
c3 SENTENCE -> [SENTENCE] -> [SENTENCE]
forall a. a -> [a] -> [a]
: [SENTENCE]
npl)
                (SENTENCE -> SENTENCE) -> SENTENCE -> SENTENCE
forall a b. (a -> b) -> a -> b
$ TERM -> TERM -> SENTENCE
mkAE (Int -> TERM
mkNTERM Int
p) (TERM -> SENTENCE) -> TERM -> SENTENCE
forall a b. (a -> b) -> a -> b
$ Int -> TERM
mkNTERM 1
    SENTENCE -> Result SENTENCE
forall (m :: * -> *) a. Monad m => a -> m a
return (SENTENCE -> Result SENTENCE) -> SENTENCE -> Result SENTENCE
forall a b. (a -> b) -> a -> b
$ SENTENCE -> SENTENCE
mk1QU (SENTENCE -> SENTENCE) -> SENTENCE -> SENTENCE
forall a b. (a -> b) -> a -> b
$ SENTENCE -> SENTENCE -> SENTENCE
mkBI SENTENCE
nce (SENTENCE -> SENTENCE) -> SENTENCE -> SENTENCE
forall a b. (a -> b) -> a -> b
$ [NAME_OR_SEQMARK] -> SENTENCE -> SENTENCE
mkQE ((Int -> NAME_OR_SEQMARK) -> [Int] -> [NAME_OR_SEQMARK]
forall a b. (a -> b) -> [a] -> [b]
map Int -> NAME_OR_SEQMARK
mkNAME [Int]
i) (SENTENCE -> SENTENCE) -> SENTENCE -> SENTENCE
forall a b. (a -> b) -> a -> b
$ [SENTENCE] -> SENTENCE
mkBC ([SENTENCE] -> SENTENCE) -> [SENTENCE] -> SENTENCE
forall a b. (a -> b) -> a -> b
$ [SENTENCE]
pl [SENTENCE] -> [SENTENCE] -> [SENTENCE]
forall a. [a] -> [a] -> [a]
++ [SENTENCE
un]

mapSubObjProp :: Sign -> ObjectPropertyExpression -> ObjectPropertyExpression
    -> Int -> Result SENTENCE
mapSubObjProp :: Sign
-> ObjectPropertyExpression
-> ObjectPropertyExpression
-> Int
-> Result SENTENCE
mapSubObjProp cSig :: Sign
cSig sp :: ObjectPropertyExpression
sp p :: ObjectPropertyExpression
p a :: Int
a = let b :: Int
b = Int
a Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1 in do
    SENTENCE
l <- Sign -> ObjectPropertyExpression -> Int -> Int -> Result SENTENCE
mapOPE Sign
cSig ObjectPropertyExpression
sp Int
a Int
b
    SENTENCE
r <- Sign -> ObjectPropertyExpression -> Int -> Int -> Result SENTENCE
mapOPE Sign
cSig ObjectPropertyExpression
p Int
a Int
b
    SENTENCE -> Result SENTENCE
forall (m :: * -> *) a. Monad m => a -> m a
return (SENTENCE -> Result SENTENCE) -> SENTENCE -> Result SENTENCE
forall a b. (a -> b) -> a -> b
$ [NAME_OR_SEQMARK] -> SENTENCE -> SENTENCE
mkQU ((Int -> NAME_OR_SEQMARK) -> [Int] -> [NAME_OR_SEQMARK]
forall a b. (a -> b) -> [a] -> [b]
map Int -> NAME_OR_SEQMARK
mkNAME [Int
a, Int
b]) (SENTENCE -> SENTENCE) -> SENTENCE -> SENTENCE
forall a b. (a -> b) -> a -> b
$ SENTENCE -> SENTENCE -> SENTENCE
mkBI SENTENCE
l SENTENCE
r

mapSubObjPropChain :: Sign -> [ObjectPropertyExpression]
    -> ObjectPropertyExpression -> Int -> Result SENTENCE
mapSubObjPropChain :: Sign
-> [ObjectPropertyExpression]
-> ObjectPropertyExpression
-> Int
-> Result SENTENCE
mapSubObjPropChain cSig :: Sign
cSig opl :: [ObjectPropertyExpression]
opl op :: ObjectPropertyExpression
op a :: Int
a = let b :: Int
b = Int
a Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1 in do
    let vars :: [Int]
vars = [Int
a Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 2 .. Int
a Int -> Int -> Int
forall a. Num a => a -> a -> a
+ [ObjectPropertyExpression] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [ObjectPropertyExpression]
opl]
        vl :: [Int]
vl = Int
a Int -> [Int] -> [Int]
forall a. a -> [a] -> [a]
: [Int]
vars [Int] -> [Int] -> [Int]
forall a. [a] -> [a] -> [a]
++ [Int
a Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1]
    [SENTENCE]
npl <- [Result SENTENCE] -> Result [SENTENCE]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence ([Result SENTENCE] -> Result [SENTENCE])
-> [Result SENTENCE] -> Result [SENTENCE]
forall a b. (a -> b) -> a -> b
$ (ObjectPropertyExpression -> Int -> Int -> Result SENTENCE)
-> [ObjectPropertyExpression]
-> [Int]
-> [Int]
-> [Result SENTENCE]
forall a b c d. (a -> b -> c -> d) -> [a] -> [b] -> [c] -> [d]
zipWith3 (Sign -> ObjectPropertyExpression -> Int -> Int -> Result SENTENCE
mapOPE Sign
cSig) [ObjectPropertyExpression]
opl [Int]
vl ([Int] -> [Result SENTENCE]) -> [Int] -> [Result SENTENCE]
forall a b. (a -> b) -> a -> b
$ [Int] -> [Int]
forall a. [a] -> [a]
tail [Int]
vl
    SENTENCE
np <- Sign -> ObjectPropertyExpression -> Int -> Int -> Result SENTENCE
mapOPE Sign
cSig ObjectPropertyExpression
op Int
a Int
b
    let lst :: [NAME_OR_SEQMARK]
lst = (Int -> NAME_OR_SEQMARK) -> [Int] -> [NAME_OR_SEQMARK]
forall a b. (a -> b) -> [a] -> [b]
map Int -> NAME_OR_SEQMARK
mkNAME ([Int] -> [NAME_OR_SEQMARK]) -> [Int] -> [NAME_OR_SEQMARK]
forall a b. (a -> b) -> a -> b
$ Int
a Int -> [Int] -> [Int]
forall a. a -> [a] -> [a]
: Int
b Int -> [Int] -> [Int]
forall a. a -> [a] -> [a]
: [Int]
vars
    SENTENCE -> Result SENTENCE
forall (m :: * -> *) a. Monad m => a -> m a
return (SENTENCE -> Result SENTENCE) -> SENTENCE -> Result SENTENCE
forall a b. (a -> b) -> a -> b
$ [NAME_OR_SEQMARK] -> SENTENCE -> SENTENCE
mkQU [NAME_OR_SEQMARK]
lst (SENTENCE -> SENTENCE) -> SENTENCE -> SENTENCE
forall a b. (a -> b) -> a -> b
$ SENTENCE -> SENTENCE -> SENTENCE
mkBI ([SENTENCE] -> SENTENCE
mkBC [SENTENCE]
npl) SENTENCE
np

mkEDPairs :: Sign -> [Int] -> Maybe Relation -> [(SENTENCE, SENTENCE)]
    -> Result ([TEXT], Sign)
mkEDPairs :: Sign
-> [Int]
-> Maybe Relation
-> [(SENTENCE, SENTENCE)]
-> Result ([TEXT], Sign)
mkEDPairs s :: Sign
s il :: [Int]
il med :: Maybe Relation
med pairs :: [(SENTENCE, SENTENCE)]
pairs = do
    let ls :: [SENTENCE]
ls = case Relation -> Maybe Relation -> Relation
forall a. a -> Maybe a -> a
fromMaybe (String -> Relation
forall a. HasCallStack => String -> a
error "expected EDRelation") Maybe Relation
med of
         EDRelation Equivalent -> ((SENTENCE, SENTENCE) -> SENTENCE)
-> [(SENTENCE, SENTENCE)] -> [SENTENCE]
forall a b. (a -> b) -> [a] -> [b]
map ((SENTENCE -> SENTENCE -> SENTENCE)
-> (SENTENCE, SENTENCE) -> SENTENCE
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry SENTENCE -> SENTENCE -> SENTENCE
mkBB) [(SENTENCE, SENTENCE)]
pairs
         EDRelation Disjoint -> ((SENTENCE, SENTENCE) -> SENTENCE)
-> [(SENTENCE, SENTENCE)] -> [SENTENCE]
forall a b. (a -> b) -> [a] -> [b]
map (\ (x :: SENTENCE
x, y :: SENTENCE
y) -> SENTENCE -> SENTENCE
mkBN (SENTENCE -> SENTENCE) -> SENTENCE -> SENTENCE
forall a b. (a -> b) -> a -> b
$ [SENTENCE] -> SENTENCE
mkBC [SENTENCE
x, SENTENCE
y]) [(SENTENCE, SENTENCE)]
pairs
         _ -> String -> [SENTENCE]
forall a. HasCallStack => String -> a
error "expected EDRelation"
    ([TEXT], Sign) -> Result ([TEXT], Sign)
forall (m :: * -> *) a. Monad m => a -> m a
return ([[Int] -> [SENTENCE] -> TEXT
eqFB [Int]
il [SENTENCE]
ls], Sign
s)

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

    ClassAxiom ax :: ClassAxiom
ax -> case ClassAxiom
ax of 
        SubClassOf _ sub :: ClassExpression
sub sup :: ClassExpression
sup -> do
            (domT :: SENTENCE
domT, dSig :: Sign
dSig) <- Sign
-> ClassExpression -> VarOrIndi -> Int -> Result (SENTENCE, Sign)
mapDescription Sign
cSig ClassExpression
sub (Int -> VarOrIndi
OVar 1) 1
            [(SENTENCE, Sign)]
ls <- (ClassExpression -> Result (SENTENCE, Sign))
-> [ClassExpression] -> Result [(SENTENCE, Sign)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\ cd :: ClassExpression
cd -> Sign
-> ClassExpression -> VarOrIndi -> Int -> Result (SENTENCE, Sign)
mapDescription Sign
cSig ClassExpression
cd (Int -> VarOrIndi
OVar 1) 1) [ClassExpression
sup]
            Sign
rSig <- Sign -> Sign -> Result Sign
sigUnion Sign
cSig (Sign -> Sign -> Sign
unite Sign
dSig (Sign -> Sign) -> Sign -> Sign
forall a b. (a -> b) -> a -> b
$ [Sign] -> Sign
uniteL ([Sign] -> Sign) -> [Sign] -> Sign
forall a b. (a -> b) -> a -> b
$ ((SENTENCE, Sign) -> Sign) -> [(SENTENCE, Sign)] -> [Sign]
forall a b. (a -> b) -> [a] -> [b]
map (SENTENCE, Sign) -> Sign
forall a b. (a, b) -> b
snd [(SENTENCE, Sign)]
ls)
            ([TEXT], Sign) -> Result ([TEXT], Sign)
forall (m :: * -> *) a. Monad m => a -> m a
return ([SENTENCE] -> [TEXT]
msen2Txt ([SENTENCE] -> [TEXT]) -> [SENTENCE] -> [TEXT]
forall a b. (a -> b) -> a -> b
$ ((SENTENCE, Sign) -> SENTENCE) -> [(SENTENCE, Sign)] -> [SENTENCE]
forall a b. (a -> b) -> [a] -> [b]
map (SENTENCE -> SENTENCE
mk1QU (SENTENCE -> SENTENCE)
-> ((SENTENCE, Sign) -> SENTENCE) -> (SENTENCE, Sign) -> SENTENCE
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SENTENCE -> SENTENCE -> SENTENCE
mkBI SENTENCE
domT (SENTENCE -> SENTENCE)
-> ((SENTENCE, Sign) -> SENTENCE) -> (SENTENCE, Sign) -> SENTENCE
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SENTENCE, Sign) -> SENTENCE
forall a b. (a, b) -> a
fst) [(SENTENCE, Sign)]
ls, Sign
rSig)

        EquivalentClasses _ cel :: [ClassExpression]
cel -> do
            (decrsS :: [(SENTENCE, SENTENCE)]
decrsS, dSig :: Sign
dSig) <- Sign
-> Int
-> [(ClassExpression, ClassExpression)]
-> Result ([(SENTENCE, SENTENCE)], Sign)
mapDescriptionListP Sign
cSig 1 ([(ClassExpression, ClassExpression)]
 -> Result ([(SENTENCE, SENTENCE)], Sign))
-> [(ClassExpression, ClassExpression)]
-> Result ([(SENTENCE, SENTENCE)], Sign)
forall a b. (a -> b) -> a -> b
$ [ClassExpression]
-> [ClassExpression] -> [(ClassExpression, ClassExpression)]
forall t t1. [t] -> [t1] -> [(t, t1)]
comPairs [ClassExpression]
cel [ClassExpression]
cel
            Sign
-> [Int]
-> Maybe Relation
-> [(SENTENCE, SENTENCE)]
-> Result ([TEXT], Sign)
mkEDPairs Sign
dSig [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) [(SENTENCE, SENTENCE)]
decrsS

        DisjointClasses _ cel :: [ClassExpression]
cel -> do
            (decrsS :: [(SENTENCE, SENTENCE)]
decrsS, dSig :: Sign
dSig) <- Sign
-> Int
-> [(ClassExpression, ClassExpression)]
-> Result ([(SENTENCE, SENTENCE)], Sign)
mapDescriptionListP Sign
cSig 1 ([(ClassExpression, ClassExpression)]
 -> Result ([(SENTENCE, SENTENCE)], Sign))
-> [(ClassExpression, ClassExpression)]
-> Result ([(SENTENCE, SENTENCE)], Sign)
forall a b. (a -> b) -> a -> b
$ [ClassExpression]
-> [ClassExpression] -> [(ClassExpression, ClassExpression)]
forall t t1. [t] -> [t1] -> [(t, t1)]
comPairs [ClassExpression]
cel [ClassExpression]
cel
            Sign
-> [Int]
-> Maybe Relation
-> [(SENTENCE, SENTENCE)]
-> Result ([TEXT], Sign)
mkEDPairs Sign
dSig [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) [(SENTENCE, SENTENCE)]
decrsS

        DisjointUnion _ clIri :: IRI
clIri clsl :: [ClassExpression]
clsl -> do
            (decrs :: [SENTENCE]
decrs, dSig :: Sign
dSig) <- Sign -> Int -> [ClassExpression] -> Result ([SENTENCE], Sign)
mapDescriptionList Sign
cSig 1 [ClassExpression]
clsl
            (decrsS :: [(SENTENCE, SENTENCE)]
decrsS, pSig :: Sign
pSig) <- Sign
-> Int
-> [(ClassExpression, ClassExpression)]
-> Result ([(SENTENCE, SENTENCE)], Sign)
mapDescriptionListP Sign
cSig 1 ([(ClassExpression, ClassExpression)]
 -> Result ([(SENTENCE, SENTENCE)], Sign))
-> [(ClassExpression, ClassExpression)]
-> Result ([(SENTENCE, SENTENCE)], Sign)
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 :: ([SENTENCE], [SENTENCE])
decrsP = [(SENTENCE, SENTENCE)] -> ([SENTENCE], [SENTENCE])
forall a b. [(a, b)] -> ([a], [b])
unzip [(SENTENCE, SENTENCE)]
decrsS
            SENTENCE
mcls <- Sign -> IRI -> Token -> Result SENTENCE
mapClassIRI Sign
cSig IRI
clIri (Token -> Result SENTENCE) -> Token -> Result SENTENCE
forall a b. (a -> b) -> a -> b
$ Int -> Token
mkNName 1
            ([TEXT], Sign) -> Result ([TEXT], Sign)
forall (m :: * -> *) a. Monad m => a -> m a
return ([SENTENCE -> TEXT
senToText (SENTENCE -> TEXT) -> SENTENCE -> TEXT
forall a b. (a -> b) -> a -> b
$ SENTENCE -> SENTENCE
mk1QU (SENTENCE -> SENTENCE) -> SENTENCE -> SENTENCE
forall a b. (a -> b) -> a -> b
$ SENTENCE -> SENTENCE -> SENTENCE
mkBB SENTENCE
mcls (SENTENCE -> SENTENCE) -> SENTENCE -> SENTENCE
forall a b. (a -> b) -> a -> b
$ [SENTENCE] -> SENTENCE
mkBC
                    [[SENTENCE] -> SENTENCE
mkBD [SENTENCE]
decrs, SENTENCE -> SENTENCE
mkBN (SENTENCE -> SENTENCE) -> SENTENCE -> SENTENCE
forall a b. (a -> b) -> a -> b
$ [SENTENCE] -> SENTENCE
mkBC ([SENTENCE] -> SENTENCE) -> [SENTENCE] -> SENTENCE
forall a b. (a -> b) -> a -> b
$ ([SENTENCE] -> [SENTENCE] -> [SENTENCE])
-> ([SENTENCE], [SENTENCE]) -> [SENTENCE]
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry [SENTENCE] -> [SENTENCE] -> [SENTENCE]
forall a. [a] -> [a] -> [a]
(++) ([SENTENCE], [SENTENCE])
decrsP]],
                    Sign -> Sign -> Sign
unite Sign
dSig Sign
pSig)

    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
                [SENTENCE]
os <- ((ObjectPropertyExpression, ObjectPropertyExpression)
 -> Result SENTENCE)
-> [(ObjectPropertyExpression, ObjectPropertyExpression)]
-> Result [SENTENCE]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\ (o1 :: ObjectPropertyExpression
o1, o2 :: ObjectPropertyExpression
o2) -> Sign
-> ObjectPropertyExpression
-> ObjectPropertyExpression
-> Int
-> Result SENTENCE
mapSubObjProp Sign
cSig ObjectPropertyExpression
o1 ObjectPropertyExpression
o2 3)
                        ([(ObjectPropertyExpression, ObjectPropertyExpression)]
 -> Result [SENTENCE])
-> [(ObjectPropertyExpression, ObjectPropertyExpression)]
-> Result [SENTENCE]
forall a b. (a -> b) -> a -> b
$ ObjectPropertyExpression
-> [ObjectPropertyExpression]
-> [(ObjectPropertyExpression, ObjectPropertyExpression)]
forall t t1. t -> [t1] -> [(t, t1)]
mkPairs ObjectPropertyExpression
opExpr [ObjectPropertyExpression
supOpExpr]
                ([TEXT], Sign) -> Result ([TEXT], Sign)
forall (m :: * -> *) a. Monad m => a -> m a
return ([SENTENCE] -> [TEXT]
msen2Txt [SENTENCE]
os, Sign
cSig)

            SubObjPropExpr_exprchain opExprs :: [ObjectPropertyExpression]
opExprs -> do
                SENTENCE
os <- Sign
-> [ObjectPropertyExpression]
-> ObjectPropertyExpression
-> Int
-> Result SENTENCE
mapSubObjPropChain Sign
cSig [ObjectPropertyExpression]
opExprs ObjectPropertyExpression
supOpExpr 3
                ([TEXT], Sign) -> Result ([TEXT], Sign)
forall (m :: * -> *) a. Monad m => a -> m a
return ([SENTENCE -> TEXT
senToText SENTENCE
os], Sign
cSig)

        EquivalentObjectProperties _ opExprs :: [ObjectPropertyExpression]
opExprs -> do
            [(SENTENCE, SENTENCE)]
pairs <- Sign
-> Int
-> Int
-> [(ObjectPropertyExpression, ObjectPropertyExpression)]
-> Result [(SENTENCE, SENTENCE)]
mapObjPropListP Sign
cSig 1 2 ([(ObjectPropertyExpression, ObjectPropertyExpression)]
 -> Result [(SENTENCE, SENTENCE)])
-> [(ObjectPropertyExpression, ObjectPropertyExpression)]
-> Result [(SENTENCE, SENTENCE)]
forall a b. (a -> b) -> a -> b
$ [ObjectPropertyExpression]
-> [ObjectPropertyExpression]
-> [(ObjectPropertyExpression, ObjectPropertyExpression)]
forall t t1. [t] -> [t1] -> [(t, t1)]
comPairs [ObjectPropertyExpression]
opExprs [ObjectPropertyExpression]
opExprs
            Sign
-> [Int]
-> Maybe Relation
-> [(SENTENCE, SENTENCE)]
-> Result ([TEXT], Sign)
mkEDPairs Sign
cSig [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) [(SENTENCE, SENTENCE)]
pairs

        DisjointObjectProperties _ opExprs :: [ObjectPropertyExpression]
opExprs -> do
            [(SENTENCE, SENTENCE)]
pairs <- Sign
-> Int
-> Int
-> [(ObjectPropertyExpression, ObjectPropertyExpression)]
-> Result [(SENTENCE, SENTENCE)]
mapObjPropListP Sign
cSig 1 2 ([(ObjectPropertyExpression, ObjectPropertyExpression)]
 -> Result [(SENTENCE, SENTENCE)])
-> [(ObjectPropertyExpression, ObjectPropertyExpression)]
-> Result [(SENTENCE, SENTENCE)]
forall a b. (a -> b) -> a -> b
$ [ObjectPropertyExpression]
-> [ObjectPropertyExpression]
-> [(ObjectPropertyExpression, ObjectPropertyExpression)]
forall t t1. [t] -> [t1] -> [(t, t1)]
comPairs [ObjectPropertyExpression]
opExprs [ObjectPropertyExpression]
opExprs
            Sign
-> [Int]
-> Maybe Relation
-> [(SENTENCE, SENTENCE)]
-> Result ([TEXT], Sign)
mkEDPairs Sign
cSig [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) [(SENTENCE, SENTENCE)]
pairs
        
        InverseObjectProperties _ opExpr1 :: ObjectPropertyExpression
opExpr1 opExpr2 :: ObjectPropertyExpression
opExpr2 -> do
            [SENTENCE]
os1 <- (ObjectPropertyExpression -> Result SENTENCE)
-> [ObjectPropertyExpression] -> Result [SENTENCE]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\ o1 :: ObjectPropertyExpression
o1 -> Sign -> ObjectPropertyExpression -> Int -> Int -> Result SENTENCE
mapOPE Sign
cSig ObjectPropertyExpression
o1 1 2) [ObjectPropertyExpression
opExpr2]
            SENTENCE
o2 <- Sign -> ObjectPropertyExpression -> Int -> Int -> Result SENTENCE
mapOPE Sign
cSig ObjectPropertyExpression
opExpr1 2 1
            ([TEXT], Sign) -> Result ([TEXT], Sign)
forall (m :: * -> *) a. Monad m => a -> m a
return ([SENTENCE] -> [TEXT]
msen2Txt ([SENTENCE] -> [TEXT]) -> [SENTENCE] -> [TEXT]
forall a b. (a -> b) -> a -> b
$ (SENTENCE -> SENTENCE) -> [SENTENCE] -> [SENTENCE]
forall a b. (a -> b) -> [a] -> [b]
map (\ cd :: SENTENCE
cd -> [NAME_OR_SEQMARK] -> SENTENCE -> SENTENCE
mkQU ((Int -> NAME_OR_SEQMARK) -> [Int] -> [NAME_OR_SEQMARK]
forall a b. (a -> b) -> [a] -> [b]
map Int -> NAME_OR_SEQMARK
mkNAME [1, 2])
                (SENTENCE -> SENTENCE) -> SENTENCE -> SENTENCE
forall a b. (a -> b) -> a -> b
$ SENTENCE -> SENTENCE -> SENTENCE
mkBB SENTENCE
cd SENTENCE
o2) [SENTENCE]
os1, Sign
cSig)

        ObjectPropertyDomain _ opExpr :: ObjectPropertyExpression
opExpr clExpr :: ClassExpression
clExpr -> do
            SENTENCE
tobjP <- Sign -> ObjectPropertyExpression -> Int -> Int -> Result SENTENCE
mapOPE Sign
cSig ObjectPropertyExpression
opExpr 1 2
            [(SENTENCE, Sign)]
tdsc <- (ClassExpression -> Result (SENTENCE, Sign))
-> [ClassExpression] -> Result [(SENTENCE, Sign)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\c :: ClassExpression
c -> Sign
-> ClassExpression -> VarOrIndi -> Int -> Result (SENTENCE, Sign)
mapDescription Sign
cSig ClassExpression
c (Int -> VarOrIndi
OVar 1) 1) [ClassExpression
clExpr]
            let vars :: (Int, Int)
vars = (1, 2)
            ([TEXT], Sign) -> Result ([TEXT], Sign)
forall (m :: * -> *) a. Monad m => a -> m a
return ([SENTENCE] -> [TEXT]
msen2Txt ([SENTENCE] -> [TEXT]) -> [SENTENCE] -> [TEXT]
forall a b. (a -> b) -> a -> b
$ ((SENTENCE, Sign) -> SENTENCE) -> [(SENTENCE, Sign)] -> [SENTENCE]
forall a b. (a -> b) -> [a] -> [b]
map ([NAME_OR_SEQMARK]
-> [NAME_OR_SEQMARK] -> SENTENCE -> SENTENCE -> SENTENCE
mkSent [Int -> NAME_OR_SEQMARK
mkNAME (Int -> NAME_OR_SEQMARK) -> Int -> NAME_OR_SEQMARK
forall a b. (a -> b) -> a -> b
$ (Int, Int) -> Int
forall a b. (a, b) -> a
fst (Int, Int)
vars]
                        [Int -> NAME_OR_SEQMARK
mkNAME (Int -> NAME_OR_SEQMARK) -> Int -> NAME_OR_SEQMARK
forall a b. (a -> b) -> a -> b
$ (Int, Int) -> Int
forall a b. (a, b) -> b
snd (Int, Int)
vars] SENTENCE
tobjP (SENTENCE -> SENTENCE)
-> ((SENTENCE, Sign) -> SENTENCE) -> (SENTENCE, Sign) -> SENTENCE
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SENTENCE, Sign) -> SENTENCE
forall a b. (a, b) -> a
fst) [(SENTENCE, Sign)]
tdsc,
                    [Sign] -> Sign
uniteL ([Sign] -> Sign) -> [Sign] -> Sign
forall a b. (a -> b) -> a -> b
$ ((SENTENCE, Sign) -> Sign) -> [(SENTENCE, Sign)] -> [Sign]
forall a b. (a -> b) -> [a] -> [b]
map (SENTENCE, Sign) -> Sign
forall a b. (a, b) -> b
snd [(SENTENCE, Sign)]
tdsc)

        ObjectPropertyRange _ opExpr :: ObjectPropertyExpression
opExpr clExpr :: ClassExpression
clExpr -> do
            SENTENCE
tobjP <- Sign -> ObjectPropertyExpression -> Int -> Int -> Result SENTENCE
mapOPE Sign
cSig ObjectPropertyExpression
opExpr 1 2
            [(SENTENCE, Sign)]
tdsc <- (ClassExpression -> Result (SENTENCE, Sign))
-> [ClassExpression] -> Result [(SENTENCE, Sign)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\c :: ClassExpression
c -> Sign
-> ClassExpression -> VarOrIndi -> Int -> Result (SENTENCE, Sign)
mapDescription Sign
cSig ClassExpression
c (Int -> VarOrIndi
OVar 2) 2) [ClassExpression
clExpr]
            let vars :: (Int, Int)
vars = (2, 1)
            ([TEXT], Sign) -> Result ([TEXT], Sign)
forall (m :: * -> *) a. Monad m => a -> m a
return ([SENTENCE] -> [TEXT]
msen2Txt ([SENTENCE] -> [TEXT]) -> [SENTENCE] -> [TEXT]
forall a b. (a -> b) -> a -> b
$ ((SENTENCE, Sign) -> SENTENCE) -> [(SENTENCE, Sign)] -> [SENTENCE]
forall a b. (a -> b) -> [a] -> [b]
map ([NAME_OR_SEQMARK]
-> [NAME_OR_SEQMARK] -> SENTENCE -> SENTENCE -> SENTENCE
mkSent [Int -> NAME_OR_SEQMARK
mkNAME (Int -> NAME_OR_SEQMARK) -> Int -> NAME_OR_SEQMARK
forall a b. (a -> b) -> a -> b
$ (Int, Int) -> Int
forall a b. (a, b) -> a
fst (Int, Int)
vars]
                        [Int -> NAME_OR_SEQMARK
mkNAME (Int -> NAME_OR_SEQMARK) -> Int -> NAME_OR_SEQMARK
forall a b. (a -> b) -> a -> b
$ (Int, Int) -> Int
forall a b. (a, b) -> b
snd (Int, Int)
vars] SENTENCE
tobjP (SENTENCE -> SENTENCE)
-> ((SENTENCE, Sign) -> SENTENCE) -> (SENTENCE, Sign) -> SENTENCE
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SENTENCE, Sign) -> SENTENCE
forall a b. (a, b) -> a
fst) [(SENTENCE, Sign)]
tdsc,
                    [Sign] -> Sign
uniteL ([Sign] -> Sign) -> [Sign] -> Sign
forall a b. (a -> b) -> a -> b
$ ((SENTENCE, Sign) -> Sign) -> [(SENTENCE, Sign)] -> [Sign]
forall a b. (a -> b) -> [a] -> [b]
map (SENTENCE, Sign) -> Sign
forall a b. (a, b) -> b
snd [(SENTENCE, Sign)]
tdsc)

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

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

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

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

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

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

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

    DataPropertyAxiom dpAxiom :: DataPropertyAxiom
dpAxiom -> case DataPropertyAxiom
dpAxiom of
        SubDataPropertyOf _ subDpExpr :: IRI
subDpExpr supDpExpr :: IRI
supDpExpr -> do
            [SENTENCE]
os1 <- (IRI -> Result SENTENCE) -> [IRI] -> Result [SENTENCE]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\ o1 :: IRI
o1 -> Sign -> IRI -> Int -> Int -> Result SENTENCE
mapDPE Sign
cSig IRI
o1 1 2) [IRI
supDpExpr]
            SENTENCE
o2 <- Sign -> IRI -> Int -> Int -> Result SENTENCE
mapDPE Sign
cSig IRI
subDpExpr 1 2
            ([TEXT], Sign) -> Result ([TEXT], Sign)
forall (m :: * -> *) a. Monad m => a -> m a
return ([SENTENCE] -> [TEXT]
msen2Txt ([SENTENCE] -> [TEXT]) -> [SENTENCE] -> [TEXT]
forall a b. (a -> b) -> a -> b
$ (SENTENCE -> SENTENCE) -> [SENTENCE] -> [SENTENCE]
forall a b. (a -> b) -> [a] -> [b]
map ([NAME_OR_SEQMARK] -> SENTENCE -> SENTENCE
mkQU ((Int -> NAME_OR_SEQMARK) -> [Int] -> [NAME_OR_SEQMARK]
forall a b. (a -> b) -> [a] -> [b]
map Int -> NAME_OR_SEQMARK
mkNAME [1, 2])
                (SENTENCE -> SENTENCE)
-> (SENTENCE -> SENTENCE) -> SENTENCE -> SENTENCE
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SENTENCE -> SENTENCE -> SENTENCE
mkBI SENTENCE
o2) [SENTENCE]
os1, Sign
cSig)

        EquivalentDataProperties _ dpExprs :: [IRI]
dpExprs -> do
            [(SENTENCE, SENTENCE)]
pairs <- Sign -> Int -> Int -> [(IRI, IRI)] -> Result [(SENTENCE, SENTENCE)]
mapDataPropListP Sign
cSig 1 2 ([(IRI, IRI)] -> Result [(SENTENCE, SENTENCE)])
-> [(IRI, IRI)] -> Result [(SENTENCE, SENTENCE)]
forall a b. (a -> b) -> a -> b
$ [IRI] -> [IRI] -> [(IRI, IRI)]
forall t t1. [t] -> [t1] -> [(t, t1)]
comPairs [IRI]
dpExprs [IRI]
dpExprs
            Sign
-> [Int]
-> Maybe Relation
-> [(SENTENCE, SENTENCE)]
-> Result ([TEXT], Sign)
mkEDPairs Sign
cSig [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) [(SENTENCE, SENTENCE)]
pairs

        DisjointDataProperties _ dpExprs :: [IRI]
dpExprs -> do
            [(SENTENCE, SENTENCE)]
pairs <- Sign -> Int -> Int -> [(IRI, IRI)] -> Result [(SENTENCE, SENTENCE)]
mapDataPropListP Sign
cSig 1 2 ([(IRI, IRI)] -> Result [(SENTENCE, SENTENCE)])
-> [(IRI, IRI)] -> Result [(SENTENCE, SENTENCE)]
forall a b. (a -> b) -> a -> b
$ [IRI] -> [IRI] -> [(IRI, IRI)]
forall t t1. [t] -> [t1] -> [(t, t1)]
comPairs [IRI]
dpExprs [IRI]
dpExprs
            Sign
-> [Int]
-> Maybe Relation
-> [(SENTENCE, SENTENCE)]
-> Result ([TEXT], Sign)
mkEDPairs Sign
cSig [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) [(SENTENCE, SENTENCE)]
pairs

        DataPropertyDomain _ dpExpr :: IRI
dpExpr clExpr :: ClassExpression
clExpr -> do
            [(SENTENCE, Sign)]
ls <- (ClassExpression -> Result (SENTENCE, Sign))
-> [ClassExpression] -> Result [(SENTENCE, Sign)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\c :: ClassExpression
c -> Sign
-> ClassExpression -> VarOrIndi -> Int -> Result (SENTENCE, Sign)
mapDescription Sign
cSig ClassExpression
c (IRI -> VarOrIndi
OIndi IRI
dpExpr) 1) [ClassExpression
clExpr]
            SENTENCE
oEx <- Sign -> IRI -> Int -> Int -> Result SENTENCE
mapDPE Sign
cSig IRI
dpExpr 1 2
            ([TEXT], Sign) -> Result ([TEXT], Sign)
forall (m :: * -> *) a. Monad m => a -> m a
return ([SENTENCE] -> [TEXT]
msen2Txt ([SENTENCE] -> [TEXT]) -> [SENTENCE] -> [TEXT]
forall a b. (a -> b) -> a -> b
$ ((SENTENCE, Sign) -> SENTENCE) -> [(SENTENCE, Sign)] -> [SENTENCE]
forall a b. (a -> b) -> [a] -> [b]
map ([NAME_OR_SEQMARK]
-> [NAME_OR_SEQMARK] -> SENTENCE -> SENTENCE -> SENTENCE
mkSent [NAME_OR_SEQMARK
mk1NAME] [Int -> NAME_OR_SEQMARK
mkNAME 2] SENTENCE
oEx
                    (SENTENCE -> SENTENCE)
-> ((SENTENCE, Sign) -> SENTENCE) -> (SENTENCE, Sign) -> SENTENCE
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SENTENCE, Sign) -> SENTENCE
forall a b. (a, b) -> a
fst) [(SENTENCE, Sign)]
ls, [Sign] -> Sign
uniteL ([Sign] -> Sign) -> [Sign] -> Sign
forall a b. (a -> b) -> a -> b
$ ((SENTENCE, Sign) -> Sign) -> [(SENTENCE, Sign)] -> [Sign]
forall a b. (a -> b) -> [a] -> [b]
map (SENTENCE, Sign) -> Sign
forall a b. (a, b) -> b
snd [(SENTENCE, Sign)]
ls)

        DataPropertyRange _ dpExpr :: IRI
dpExpr dr :: DataRange
dr -> do
            SENTENCE
oEx <- Sign -> IRI -> Int -> Int -> Result SENTENCE
mapDPE Sign
cSig IRI
dpExpr 1 2
            [(SENTENCE, Sign)]
ls <- (DataRange -> Result (SENTENCE, Sign))
-> [DataRange] -> Result [(SENTENCE, Sign)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\r :: DataRange
r-> Sign -> DataRange -> VarOrIndi -> Result (SENTENCE, Sign)
mapDataRange Sign
cSig DataRange
r (VarOrIndi -> Result (SENTENCE, Sign))
-> VarOrIndi -> Result (SENTENCE, Sign)
forall a b. (a -> b) -> a -> b
$ Int -> VarOrIndi
OVar 2) [DataRange
dr]
            ([TEXT], Sign) -> Result ([TEXT], Sign)
forall (m :: * -> *) a. Monad m => a -> m a
return ([SENTENCE] -> [TEXT]
msen2Txt ([SENTENCE] -> [TEXT]) -> [SENTENCE] -> [TEXT]
forall a b. (a -> b) -> a -> b
$ ((SENTENCE, Sign) -> SENTENCE) -> [(SENTENCE, Sign)] -> [SENTENCE]
forall a b. (a -> b) -> [a] -> [b]
map ([NAME_OR_SEQMARK]
-> [NAME_OR_SEQMARK] -> SENTENCE -> SENTENCE -> SENTENCE
mkSent [Int -> NAME_OR_SEQMARK
mkNAME 1] [Int -> NAME_OR_SEQMARK
mkNAME 2] SENTENCE
oEx
                        (SENTENCE -> SENTENCE)
-> ((SENTENCE, Sign) -> SENTENCE) -> (SENTENCE, Sign) -> SENTENCE
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SENTENCE, Sign) -> SENTENCE
forall a b. (a, b) -> a
fst) [(SENTENCE, Sign)]
ls, [Sign] -> Sign
uniteL ([Sign] -> Sign) -> [Sign] -> Sign
forall a b. (a -> b) -> a -> b
$ ((SENTENCE, Sign) -> Sign) -> [(SENTENCE, Sign)] -> [Sign]
forall a b. (a -> b) -> [a] -> [b]
map (SENTENCE, Sign) -> Sign
forall a b. (a, b) -> b
snd [(SENTENCE, Sign)]
ls )

        FunctionalDataProperty _ dpExpr :: IRI
dpExpr -> do
            SENTENCE
so1 <- Sign -> IRI -> Int -> Int -> Result SENTENCE
mapDPE Sign
cSig IRI
dpExpr 1 2
            SENTENCE
so2 <- Sign -> IRI -> Int -> Int -> Result SENTENCE
mapDPE Sign
cSig IRI
dpExpr 1 3
            ([TEXT], Sign) -> Result ([TEXT], Sign)
forall (m :: * -> *) a. Monad m => a -> m a
return ([[NAME_OR_SEQMARK] -> [SENTENCE] -> TERM -> TERM -> TEXT
mkQUBI ((Int -> NAME_OR_SEQMARK) -> [Int] -> [NAME_OR_SEQMARK]
forall a b. (a -> b) -> [a] -> [b]
map Int -> NAME_OR_SEQMARK
mkNAME [1, 2, 3]) [SENTENCE
so1, SENTENCE
so2]
                            (Int -> TERM
mkNTERM 2) (TERM -> TEXT) -> TERM -> TEXT
forall a b. (a -> b) -> a -> b
$ Int -> TERM
mkNTERM 3], Sign
cSig)

    DatatypeDefinition _ dt :: IRI
dt dr :: DataRange
dr -> do
        (odes :: SENTENCE
odes, dSig :: Sign
dSig) <- Sign -> DataRange -> VarOrIndi -> Result (SENTENCE, Sign)
mapDataRange Sign
cSig DataRange
dr (VarOrIndi -> Result (SENTENCE, Sign))
-> VarOrIndi -> Result (SENTENCE, Sign)
forall a b. (a -> b) -> a -> b
$ Int -> VarOrIndi
OVar 1
        let dtp :: SENTENCE
dtp = Token -> [TERM] -> SENTENCE
mkTermAtoms (IRI -> Token
uriToTok IRI
dt) [VarOrIndi -> TERM
mkVTerm (VarOrIndi -> TERM) -> VarOrIndi -> TERM
forall a b. (a -> b) -> a -> b
$ Int -> VarOrIndi
OVar 1]
        ([TEXT], Sign) -> Result ([TEXT], Sign)
forall (m :: * -> *) a. Monad m => a -> m a
return ([SENTENCE -> TEXT
senToText (SENTENCE -> TEXT) -> SENTENCE -> TEXT
forall a b. (a -> b) -> a -> b
$ SENTENCE -> SENTENCE
mk1QU (SENTENCE -> SENTENCE) -> SENTENCE -> SENTENCE
forall a b. (a -> b) -> a -> b
$ SENTENCE -> SENTENCE -> SENTENCE
mkBB SENTENCE
dtp SENTENCE
odes], Sign
dSig)

    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
        (_, sig :: Sign
sig) <- Sign
-> ClassExpression -> VarOrIndi -> Int -> Result (SENTENCE, Sign)
mapDescription Sign
cSig ClassExpression
ce (Int -> VarOrIndi
OVar 1) 1
        [SENTENCE]
ol <- ((Int, ObjectPropertyExpression) -> Result SENTENCE)
-> [(Int, ObjectPropertyExpression)] -> Result [SENTENCE]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\ (n :: Int
n, o :: ObjectPropertyExpression
o) -> Sign -> ObjectPropertyExpression -> Int -> Int -> Result SENTENCE
mapOPE Sign
cSig ObjectPropertyExpression
o 1 Int
n) ([(Int, ObjectPropertyExpression)] -> Result [SENTENCE])
-> [(Int, ObjectPropertyExpression)] -> Result [SENTENCE]
forall a b. (a -> b) -> a -> b
$ [Int]
-> [ObjectPropertyExpression] -> [(Int, ObjectPropertyExpression)]
forall t t1. [t] -> [t1] -> [(t, t1)]
zip [Int]
uptoOP [ObjectPropertyExpression]
opl
        [SENTENCE]
nol <- ((Int, ObjectPropertyExpression) -> Result SENTENCE)
-> [(Int, ObjectPropertyExpression)] -> Result [SENTENCE]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\ (n :: Int
n, o :: ObjectPropertyExpression
o) -> Sign -> ObjectPropertyExpression -> Int -> Int -> Result SENTENCE
mapOPE Sign
cSig ObjectPropertyExpression
o Int
tl Int
n) ([(Int, ObjectPropertyExpression)] -> Result [SENTENCE])
-> [(Int, ObjectPropertyExpression)] -> Result [SENTENCE]
forall a b. (a -> b) -> a -> b
$ [Int]
-> [ObjectPropertyExpression] -> [(Int, ObjectPropertyExpression)]
forall t t1. [t] -> [t1] -> [(t, t1)]
zip [Int]
uptoOP [ObjectPropertyExpression]
opl
        [SENTENCE]
dl <- ((Int, IRI) -> Result SENTENCE)
-> [(Int, IRI)] -> Result [SENTENCE]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\ (n :: Int
n, d :: IRI
d) -> Sign -> IRI -> Int -> Int -> Result SENTENCE
mapDPE Sign
cSig IRI
d 1 Int
n) ([(Int, IRI)] -> Result [SENTENCE])
-> [(Int, IRI)] -> Result [SENTENCE]
forall a b. (a -> b) -> a -> b
$ [Int] -> [IRI] -> [(Int, IRI)]
forall t t1. [t] -> [t1] -> [(t, t1)]
zip [Int]
uptoDP [IRI]
dpl
        [SENTENCE]
ndl <- ((Int, IRI) -> Result SENTENCE)
-> [(Int, IRI)] -> Result [SENTENCE]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\ (n :: Int
n, d :: IRI
d) -> Sign -> IRI -> Int -> Int -> Result SENTENCE
mapDPE Sign
cSig IRI
d Int
tl Int
n) ([(Int, IRI)] -> Result [SENTENCE])
-> [(Int, IRI)] -> Result [SENTENCE]
forall a b. (a -> b) -> a -> b
$ [Int] -> [IRI] -> [(Int, IRI)]
forall t t1. [t] -> [t1] -> [(t, t1)]
zip [Int]
uptoDP [IRI]
dpl
        SENTENCE
keys <- Sign
-> ClassExpression
-> ([SENTENCE], [SENTENCE])
-> Int
-> [Int]
-> Result SENTENCE
mapKey Sign
cSig ClassExpression
ce ([SENTENCE]
ol [SENTENCE] -> [SENTENCE] -> [SENTENCE]
forall a. [a] -> [a] -> [a]
++ [SENTENCE]
dl, [SENTENCE]
nol [SENTENCE] -> [SENTENCE] -> [SENTENCE]
forall a. [a] -> [a] -> [a]
++ [SENTENCE]
ndl) Int
tl
            ([Int] -> Result SENTENCE) -> [Int] -> Result SENTENCE
forall a b. (a -> b) -> a -> b
$ [Int]
uptoOP [Int] -> [Int] -> [Int]
forall a. [a] -> [a] -> [a]
++ [Int]
uptoDP
        ([TEXT], Sign) -> Result ([TEXT], Sign)
forall (m :: * -> *) a. Monad m => a -> m a
return ([SENTENCE -> TEXT
senToText SENTENCE
keys], Sign
sig)

    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:t :: [IRI]
t) -> (IRI -> Maybe IRI
forall a. a -> Maybe a
Just IRI
iri, [IRI]
t)
                    _ -> (Maybe IRI
forall a. Maybe a
Nothing, [IRI]
inds)
            [SENTENCE]
fs <- Sign -> SameOrDifferent -> Maybe IRI -> [IRI] -> Result [SENTENCE]
mapComIndivList Sign
cSig SameOrDifferent
Same Maybe IRI
mi [IRI]
rest
            ([TEXT], Sign) -> Result ([TEXT], Sign)
forall (m :: * -> *) a. Monad m => a -> m a
return ([SENTENCE] -> [TEXT]
msen2Txt [SENTENCE]
fs, Sign
cSig)

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

        ClassAssertion _ ce :: ClassExpression
ce iIri :: IRI
iIri -> do
            (SENTENCE, Sign)
l <- Sign
-> ClassExpression -> VarOrIndi -> Int -> Result (SENTENCE, Sign)
mapDescription Sign
cSig ClassExpression
ce (IRI -> VarOrIndi
OIndi IRI
iIri) 1
            TERM
inD <- Sign -> IRI -> Result TERM
mapIndivIRI Sign
cSig IRI
iIri
            let ocl :: TEXT
ocl = TERM -> (ClassExpression, SENTENCE) -> TEXT
mapClassAssertion TERM
inD (ClassExpression
ce, (SENTENCE, Sign) -> SENTENCE
forall a b. (a, b) -> a
fst (SENTENCE, Sign)
l)
            ([TEXT], Sign) -> Result ([TEXT], Sign)
forall (m :: * -> *) a. Monad m => a -> m a
return ([TEXT
ocl], (SENTENCE, Sign) -> Sign
forall a b. (a, b) -> b
snd (SENTENCE, Sign)
l)

        ObjectPropertyAssertion _ op :: ObjectPropertyExpression
op si :: IRI
si ti :: IRI
ti -> do
            SENTENCE
oPropH <- Sign
-> ObjectPropertyExpression
-> VarOrIndi
-> VarOrIndi
-> Result SENTENCE
mapObjProp Sign
cSig ObjectPropertyExpression
op (IRI -> VarOrIndi
OIndi IRI
si) (IRI -> VarOrIndi
OIndi IRI
ti)
            ([TEXT], Sign) -> Result ([TEXT], Sign)
forall (m :: * -> *) a. Monad m => a -> m a
return ([SENTENCE -> TEXT
senToText (SENTENCE -> TEXT) -> SENTENCE -> TEXT
forall a b. (a -> b) -> a -> b
$ SENTENCE
oPropH], Sign
cSig)

        NegativeObjectPropertyAssertion _ op :: ObjectPropertyExpression
op si :: IRI
si ti :: IRI
ti -> do
            SENTENCE
oPropH <- Sign
-> ObjectPropertyExpression
-> VarOrIndi
-> VarOrIndi
-> Result SENTENCE
mapObjProp Sign
cSig ObjectPropertyExpression
op (IRI -> VarOrIndi
OIndi IRI
si) (IRI -> VarOrIndi
OIndi IRI
ti)
            ([TEXT], Sign) -> Result ([TEXT], Sign)
forall (m :: * -> *) a. Monad m => a -> m a
return ([SENTENCE -> TEXT
senToText (SENTENCE -> TEXT) -> SENTENCE -> TEXT
forall a b. (a -> b) -> a -> b
$ SENTENCE -> SENTENCE
mkBN (SENTENCE -> SENTENCE) -> SENTENCE -> SENTENCE
forall a b. (a -> b) -> a -> b
$ SENTENCE
oPropH], Sign
cSig)

        DataPropertyAssertion _ dp :: IRI
dp si :: IRI
si tv :: Literal
tv -> do
            TERM
inS <- Sign -> IRI -> Result TERM
mapIndivIRI Sign
cSig IRI
si
            Either (SENTENCE, SENTENCE) TERM
inT <- Int -> Literal -> Result (Either (SENTENCE, SENTENCE) TERM)
mapLit 1 Literal
tv
            Token
nm <- IRI -> Result Token
uriToTokM IRI
dp
            SENTENCE
dPropH <- case Either (SENTENCE, SENTENCE) TERM
inT of
                    Right li :: TERM
li -> SENTENCE -> Result SENTENCE
forall (m :: * -> *) a. Monad m => a -> m a
return (SENTENCE -> Result SENTENCE) -> SENTENCE -> Result SENTENCE
forall a b. (a -> b) -> a -> b
$ Token -> [TERM] -> SENTENCE
mkTermAtoms Token
nm [TERM
inS, TERM
li]
                    Left (s1 :: SENTENCE
s1, s2 :: SENTENCE
s2) -> do
                        SENTENCE
sens <- Sign -> IRI -> VarOrIndi -> VarOrIndi -> Result SENTENCE
mapDataProp Sign
cSig IRI
dp (IRI -> VarOrIndi
OIndi IRI
si) (VarOrIndi -> Result SENTENCE) -> VarOrIndi -> Result SENTENCE
forall a b. (a -> b) -> a -> b
$ Int -> VarOrIndi
OVar 1
                        SENTENCE -> Result SENTENCE
forall (m :: * -> *) a. Monad m => a -> m a
return (SENTENCE -> Result SENTENCE) -> SENTENCE -> Result SENTENCE
forall a b. (a -> b) -> a -> b
$ [SENTENCE] -> SENTENCE
mkBC [SENTENCE
sens, SENTENCE
s1, SENTENCE
s2]
            ([TEXT], Sign) -> Result ([TEXT], Sign)
forall (m :: * -> *) a. Monad m => a -> m a
return ([SENTENCE -> TEXT
senToText (SENTENCE -> TEXT) -> SENTENCE -> TEXT
forall a b. (a -> b) -> a -> b
$ SENTENCE
dPropH], Sign
cSig)

        NegativeDataPropertyAssertion _ dp :: IRI
dp si :: IRI
si tv :: Literal
tv -> do
            TERM
inS <- Sign -> IRI -> Result TERM
mapIndivIRI Sign
cSig IRI
si
            Either (SENTENCE, SENTENCE) TERM
inT <- Int -> Literal -> Result (Either (SENTENCE, SENTENCE) TERM)
mapLit 1 Literal
tv
            Token
nm <- IRI -> Result Token
uriToTokM IRI
dp
            SENTENCE
dPropH <- case Either (SENTENCE, SENTENCE) TERM
inT of
                    Right li :: TERM
li -> SENTENCE -> Result SENTENCE
forall (m :: * -> *) a. Monad m => a -> m a
return (SENTENCE -> Result SENTENCE) -> SENTENCE -> Result SENTENCE
forall a b. (a -> b) -> a -> b
$ Token -> [TERM] -> SENTENCE
mkTermAtoms Token
nm [TERM
inS, TERM
li]
                    Left (s1 :: SENTENCE
s1, s2 :: SENTENCE
s2) -> do
                        SENTENCE
sens <- Sign -> IRI -> VarOrIndi -> VarOrIndi -> Result SENTENCE
mapDataProp Sign
cSig IRI
dp (IRI -> VarOrIndi
OIndi IRI
si) (VarOrIndi -> Result SENTENCE) -> VarOrIndi -> Result SENTENCE
forall a b. (a -> b) -> a -> b
$ Int -> VarOrIndi
OVar 1
                        SENTENCE -> Result SENTENCE
forall (m :: * -> *) a. Monad m => a -> m a
return (SENTENCE -> Result SENTENCE) -> SENTENCE -> Result SENTENCE
forall a b. (a -> b) -> a -> b
$ [SENTENCE] -> SENTENCE
mkBC [SENTENCE
sens, SENTENCE
s1, SENTENCE
s2]
            ([TEXT], Sign) -> Result ([TEXT], Sign)
forall (m :: * -> *) a. Monad m => a -> m a
return ([SENTENCE -> TEXT
senToText (SENTENCE -> TEXT) -> SENTENCE -> TEXT
forall a b. (a -> b) -> a -> b
$ SENTENCE -> SENTENCE
mkBN (SENTENCE -> SENTENCE) -> SENTENCE -> SENTENCE
forall a b. (a -> b) -> a -> b
$ SENTENCE
dPropH], Sign
cSig)

    AnnotationAxiom _ -> ([TEXT], Sign) -> Result ([TEXT], Sign)
forall (m :: * -> *) a. Monad m => a -> m a
return ([], Sign
cSig)

    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 :: [NAME_OR_SEQMARK]
names = Token -> NAME_OR_SEQMARK
Name (Token -> NAME_OR_SEQMARK)
-> (IRI -> Token) -> IRI -> NAME_OR_SEQMARK
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IRI -> Token
uriToTok (IRI -> NAME_OR_SEQMARK) -> [IRI] -> [NAME_OR_SEQMARK]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [IRI]
vars
                f :: ([SENTENCE], Sign, Int) -> Atom -> Result ([SENTENCE], Sign, Int)
f (sentences :: [SENTENCE]
sentences, sig :: Sign
sig, startVal :: Int
startVal) at :: Atom
at = do
                    (sentences' :: [SENTENCE]
sentences', sig' :: Sign
sig', offsetValue :: Int
offsetValue) <- Int -> Sign -> Atom -> Result ([SENTENCE], Sign, Int)
atomToSentence Int
startVal Sign
sig Atom
at
                    ([SENTENCE], Sign, Int) -> Result ([SENTENCE], Sign, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ([SENTENCE]
sentences [SENTENCE] -> [SENTENCE] -> [SENTENCE]
forall a. [a] -> [a] -> [a]
++ [SENTENCE]
sentences', Sign
sig', Int
offsetValue)

                g :: Int -> Sign -> t Atom -> Result ([SENTENCE], Sign, Int)
g startVal :: Int
startVal sig :: Sign
sig atoms :: t Atom
atoms = (([SENTENCE], Sign, Int) -> Atom -> Result ([SENTENCE], Sign, Int))
-> ([SENTENCE], Sign, Int)
-> t Atom
-> Result ([SENTENCE], Sign, Int)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM ([SENTENCE], Sign, Int) -> Atom -> Result ([SENTENCE], Sign, Int)
f ([], Sign
sig, Int
startVal) t Atom
atoms
            in do
                (antecedentSen :: [SENTENCE]
antecedentSen, sig :: Sign
sig, offsetValue :: Int
offsetValue) <- Int -> Sign -> Body -> Result ([SENTENCE], Sign, Int)
forall (t :: * -> *).
Foldable t =>
Int -> Sign -> t Atom -> Result ([SENTENCE], Sign, Int)
g 1 Sign
cSig Body
b
                let antecedent :: SENTENCE
antecedent = case [SENTENCE]
antecedentSen of
                        [s :: SENTENCE
s] -> SENTENCE
s
                        _ -> BOOL_SENT -> SENTENCE
mkBools (BOOL_SENT -> SENTENCE) -> BOOL_SENT -> SENTENCE
forall a b. (a -> b) -> a -> b
$ [SENTENCE] -> BOOL_SENT
cnjct [SENTENCE]
antecedentSen
                    
                (consequentSen :: [SENTENCE]
consequentSen, sig' :: Sign
sig', lastVar :: Int
lastVar) <- Int -> Sign -> Body -> Result ([SENTENCE], Sign, Int)
forall (t :: * -> *).
Foldable t =>
Int -> Sign -> t Atom -> Result ([SENTENCE], Sign, Int)
g Int
offsetValue Sign
sig Body
h
                let consequent :: SENTENCE
consequent =case [SENTENCE]
consequentSen of
                        [s :: SENTENCE
s] -> SENTENCE
s
                        _ -> BOOL_SENT -> SENTENCE
mkBools (BOOL_SENT -> SENTENCE) -> BOOL_SENT -> SENTENCE
forall a b. (a -> b) -> a -> b
$ [SENTENCE] -> BOOL_SENT
cnjct [SENTENCE]
consequentSen

                
                let impl :: SENTENCE
impl = BOOL_SENT -> SENTENCE
mkBools (BOOL_SENT -> SENTENCE) -> BOOL_SENT -> SENTENCE
forall a b. (a -> b) -> a -> b
$ SENTENCE -> SENTENCE -> BOOL_SENT
mkImpl SENTENCE
antecedent SENTENCE
consequent
                ([TEXT], Sign) -> Result ([TEXT], Sign)
forall (m :: * -> *) a. Monad m => a -> m a
return (([TEXT], Sign) -> Result ([TEXT], Sign))
-> ([TEXT], Sign) -> Result ([TEXT], Sign)
forall a b. (a -> b) -> a -> b
$ ([SENTENCE -> TEXT
senToText (SENTENCE -> TEXT) -> SENTENCE -> TEXT
forall a b. (a -> b) -> a -> b
$ [NAME_OR_SEQMARK] -> SENTENCE -> Range -> SENTENCE
mkUnivQ ([NAME_OR_SEQMARK]
names [NAME_OR_SEQMARK] -> [NAME_OR_SEQMARK] -> [NAME_OR_SEQMARK]
forall a. [a] -> [a] -> [a]
++ (Int -> NAME_OR_SEQMARK) -> [Int] -> [NAME_OR_SEQMARK]
forall a b. (a -> b) -> [a] -> [b]
map Int -> NAME_OR_SEQMARK
mkNAME [1..Int
lastVar Int -> Int -> Int
forall a. Num a => a -> a -> a
- 1]) SENTENCE
impl Range
nullRange], Sign
sig')
        DGRule _ _ _ -> String -> Result ([TEXT], Sign)
forall a. HasCallStack => String -> a
error "mapAxioms: DGRules are not supported yet!"
    
    DGAxiom _ _ _ _ _ -> String -> Result ([TEXT], Sign)
forall a. HasCallStack => String -> a
error "mapAxioms: DGAxiom are not supported yet!"
        -- DGRule _  ->  -- ? Ask Mihai whether to implement and if so how? What do those represent? How to write them in Common Logic?
    -- DGAxiom _ c man   ->  -- ? Ask Mihai whether to implement and if so how?  What do those represent? How to write them in Common Logic?

iArgToTerm :: IndividualArg -> TERM
iArgToTerm :: IndividualArg -> TERM
iArgToTerm arg :: IndividualArg
arg = case IndividualArg
arg of
    IVar v :: IRI
v -> Token -> TERM
Name_term (Token -> TERM) -> (IRI -> Token) -> IRI -> TERM
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IRI -> Token
uriToTok (IRI -> TERM) -> IRI -> TERM
forall a b. (a -> b) -> a -> b
$ IRI
v
    IArg iri :: IRI
iri -> Token -> TERM
Name_term (Token -> TERM) -> (IRI -> Token) -> IRI -> TERM
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IRI -> Token
uriToTok (IRI -> TERM) -> IRI -> TERM
forall a b. (a -> b) -> a -> b
$ IRI
iri

iArgToVarOrIndi :: Int -> IndividualArg -> Result ([SENTENCE], VarOrIndi, Int)
iArgToVarOrIndi :: Int -> IndividualArg -> Result ([SENTENCE], VarOrIndi, Int)
iArgToVarOrIndi startVar :: Int
startVar arg :: IndividualArg
arg = case IndividualArg
arg of
    IVar var :: IRI
var -> ([SENTENCE], VarOrIndi, Int) -> Result ([SENTENCE], VarOrIndi, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ([], IRI -> VarOrIndi
OIndi IRI
var, Int
startVar)
    IArg iri :: IRI
iri -> ([SENTENCE], VarOrIndi, Int) -> Result ([SENTENCE], VarOrIndi, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ([], IRI -> VarOrIndi
OIndi IRI
iri, Int
startVar)

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

dArgToVarOrIndi :: Int -> DataArg -> Result ([SENTENCE], VarOrIndi, Int)
dArgToVarOrIndi :: Int -> DataArg -> Result ([SENTENCE], VarOrIndi, Int)
dArgToVarOrIndi startVar :: Int
startVar arg :: DataArg
arg = case DataArg
arg of
    DVar var :: IRI
var -> ([SENTENCE], VarOrIndi, Int) -> Result ([SENTENCE], VarOrIndi, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return (([SENTENCE], VarOrIndi, Int)
 -> Result ([SENTENCE], VarOrIndi, Int))
-> ([SENTENCE], VarOrIndi, Int)
-> Result ([SENTENCE], VarOrIndi, Int)
forall a b. (a -> b) -> a -> b
$ ([], IRI -> VarOrIndi
OIndi IRI
var, Int
startVar)
    DArg lit :: Literal
lit -> do
        let var :: VarOrIndi
var = Int -> VarOrIndi
OVar (Int -> VarOrIndi) -> Int -> VarOrIndi
forall a b. (a -> b) -> a -> b
$ Int
startVar
        let uid :: TERM
uid = VarOrIndi -> TERM
mkVTerm VarOrIndi
var
        Either (SENTENCE, SENTENCE) TERM
cl <- Int -> Literal -> Result (Either (SENTENCE, SENTENCE) TERM)
mapLit Int
startVar Literal
lit
        let sen :: SENTENCE
sen = case Either (SENTENCE, SENTENCE) TERM
cl of
                Left (sen1 :: SENTENCE
sen1, sen2 :: SENTENCE
sen2) -> [SENTENCE] -> SENTENCE
mkBC [SENTENCE
sen1,SENTENCE
sen2]
                Right term :: TERM
term -> ATOM -> SENTENCE
mkAtoms (ATOM -> SENTENCE) -> ATOM -> SENTENCE
forall a b. (a -> b) -> a -> b
$ TERM -> [TERM_SEQ] -> ATOM
Atom TERM
term [TERM -> TERM_SEQ
Term_seq TERM
uid]
        ([SENTENCE], VarOrIndi, Int) -> Result ([SENTENCE], VarOrIndi, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ([SENTENCE
sen], VarOrIndi
var, Int
startVar Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1)

-- make PROFILE=on restack
-- make PROFILE=on hets
mapClassExpression :: TERM -> (ClassExpression, SENTENCE) -> SENTENCE
mapClassExpression :: TERM -> (ClassExpression, SENTENCE) -> SENTENCE
mapClassExpression ind :: TERM
ind (ce :: ClassExpression
ce, sent :: SENTENCE
sent) = case ClassExpression
ce of
    Expression _ -> SENTENCE
sent
    _ -> (SENTENCE -> SENTENCE
mk1QU (SENTENCE -> SENTENCE)
-> (SENTENCE -> SENTENCE) -> SENTENCE -> SENTENCE
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SENTENCE -> SENTENCE -> SENTENCE
mkBI (TERM -> TERM -> SENTENCE
mkAE TERM
mk1NTERM TERM
ind)) SENTENCE
sent

atomToSentence :: Int -> Sign -> Atom -> Result ([SENTENCE], Sign, Int)
atomToSentence :: Int -> Sign -> Atom -> Result ([SENTENCE], Sign, Int)
atomToSentence startVar :: Int
startVar cSig :: Sign
cSig atom :: Atom
atom = case Atom
atom of
    ClassAtom clExpr :: ClassExpression
clExpr iarg :: IndividualArg
iarg -> do 
        (sentences :: [SENTENCE]
sentences, var :: VarOrIndi
var, offsetValue :: Int
offsetValue) <- Int -> IndividualArg -> Result ([SENTENCE], VarOrIndi, Int)
iArgToVarOrIndi Int
startVar IndividualArg
iarg
        (l :: SENTENCE
l, sig :: Sign
sig) <- Sign
-> ClassExpression -> VarOrIndi -> Int -> Result (SENTENCE, Sign)
mapDescription Sign
cSig ClassExpression
clExpr VarOrIndi
var 1
        ([SENTENCE], Sign, Int) -> Result ([SENTENCE], Sign, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return (TERM -> (ClassExpression, SENTENCE) -> SENTENCE
mapClassExpression (IndividualArg -> TERM
iArgToTerm IndividualArg
iarg) (ClassExpression
clExpr, SENTENCE
l) SENTENCE -> [SENTENCE] -> [SENTENCE]
forall a. a -> [a] -> [a]
: [SENTENCE]
sentences, Sign
sig, Int
offsetValue)
        
    DataRangeAtom dataRange :: DataRange
dataRange darg :: DataArg
darg -> do
        (sentences :: [SENTENCE]
sentences, var :: VarOrIndi
var, offsetValue :: Int
offsetValue) <- Int -> DataArg -> Result ([SENTENCE], VarOrIndi, Int)
dArgToVarOrIndi Int
startVar DataArg
darg
        (s :: SENTENCE
s, sig :: Sign
sig) <- Sign -> DataRange -> VarOrIndi -> Int -> Result (SENTENCE, Sign)
mapDataRangeAux Sign
cSig DataRange
dataRange VarOrIndi
var Int
offsetValue
        ([SENTENCE], Sign, Int) -> Result ([SENTENCE], Sign, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return (SENTENCE
s SENTENCE -> [SENTENCE] -> [SENTENCE]
forall a. a -> [a] -> [a]
: [SENTENCE]
sentences, Sign
sig, Int
offsetValue Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1)

    ObjectPropertyAtom opExpr :: ObjectPropertyExpression
opExpr iarg1 :: IndividualArg
iarg1 iarg2 :: IndividualArg
iarg2 -> do
        (sentences1 :: [SENTENCE]
sentences1, var1 :: VarOrIndi
var1, offsetValue1 :: Int
offsetValue1) <- Int -> IndividualArg -> Result ([SENTENCE], VarOrIndi, Int)
iArgToVarOrIndi Int
startVar IndividualArg
iarg1
        (sentences2 :: [SENTENCE]
sentences2, var2 :: VarOrIndi
var2, offsetValue2 :: Int
offsetValue2) <- Int -> IndividualArg -> Result ([SENTENCE], VarOrIndi, Int)
iArgToVarOrIndi Int
offsetValue1 IndividualArg
iarg2
        SENTENCE
sen <- Sign
-> ObjectPropertyExpression
-> VarOrIndi
-> VarOrIndi
-> Result SENTENCE
mapObjProp Sign
cSig ObjectPropertyExpression
opExpr VarOrIndi
var1 VarOrIndi
var2
        ([SENTENCE], Sign, Int) -> Result ([SENTENCE], Sign, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return (SENTENCE
sen SENTENCE -> [SENTENCE] -> [SENTENCE]
forall a. a -> [a] -> [a]
: [SENTENCE]
sentences1 [SENTENCE] -> [SENTENCE] -> [SENTENCE]
forall a. [a] -> [a] -> [a]
++ [SENTENCE]
sentences2 , Sign
cSig, Int
offsetValue2)

    DataPropertyAtom dpExpr :: IRI
dpExpr iarg :: IndividualArg
iarg darg :: DataArg
darg -> do
            (sentences :: [SENTENCE]
sentences, var1 :: VarOrIndi
var1, offsetValue :: Int
offsetValue) <- Int -> IndividualArg -> Result ([SENTENCE], VarOrIndi, Int)
iArgToVarOrIndi Int
startVar IndividualArg
iarg
            case DataArg
darg of
                DVar var2 :: IRI
var2 -> do
                    SENTENCE
sen <- Sign -> IRI -> VarOrIndi -> VarOrIndi -> Result SENTENCE
mapDataProp Sign
cSig IRI
dpExpr VarOrIndi
var1 (IRI -> VarOrIndi
OIndi IRI
var2)
                    ([SENTENCE], Sign, Int) -> Result ([SENTENCE], Sign, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return (SENTENCE
sen SENTENCE -> [SENTENCE] -> [SENTENCE]
forall a. a -> [a] -> [a]
: [SENTENCE]
sentences, Sign
cSig, Int
offsetValue)
                DArg lit :: Literal
lit -> do
                    Either (SENTENCE, SENTENCE) TERM
inT <- Int -> Literal -> Result (Either (SENTENCE, SENTENCE) TERM)
mapLit Int
startVar Literal
lit
                    Token
nm <- IRI -> Result Token
uriToTokM IRI
dpExpr
                    case Either (SENTENCE, SENTENCE) TERM
inT of
                            Right li :: TERM
li -> ([SENTENCE], Sign, Int) -> Result ([SENTENCE], Sign, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return (([SENTENCE], Sign, Int) -> Result ([SENTENCE], Sign, Int))
-> ([SENTENCE], Sign, Int) -> Result ([SENTENCE], Sign, Int)
forall a b. (a -> b) -> a -> b
$ (Token -> [TERM] -> SENTENCE
mkTermAtoms Token
nm [VarOrIndi -> TERM
mkVTerm VarOrIndi
var1, TERM
li] SENTENCE -> [SENTENCE] -> [SENTENCE]
forall a. a -> [a] -> [a]
: [SENTENCE]
sentences, Sign
cSig, Int
offsetValue)
                            Left (s1 :: SENTENCE
s1, s2 :: SENTENCE
s2) -> do
                                SENTENCE
sen <- Sign -> IRI -> VarOrIndi -> VarOrIndi -> Result SENTENCE
mapDataProp Sign
cSig IRI
dpExpr VarOrIndi
var1 (VarOrIndi -> Result SENTENCE) -> VarOrIndi -> Result SENTENCE
forall a b. (a -> b) -> a -> b
$ Int -> VarOrIndi
OVar (Int
offsetValue Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1)
                                ([SENTENCE], Sign, Int) -> Result ([SENTENCE], Sign, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ([SENTENCE] -> SENTENCE
mkBC [SENTENCE
sen, SENTENCE
s1, SENTENCE
s2] SENTENCE -> [SENTENCE] -> [SENTENCE]
forall a. a -> [a] -> [a]
: [SENTENCE]
sentences, Sign
cSig, Int
offsetValue Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 2)

    BuiltInAtom iri :: IRI
iri args :: [DataArg]
args -> do
        (l :: [([SENTENCE], VarOrIndi, Int)]
l, offsetValue :: Int
offsetValue) <- (([([SENTENCE], VarOrIndi, Int)], Int)
 -> DataArg -> Result ([([SENTENCE], VarOrIndi, Int)], Int))
-> ([([SENTENCE], VarOrIndi, Int)], Int)
-> [DataArg]
-> Result ([([SENTENCE], VarOrIndi, Int)], Int)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (\(results :: [([SENTENCE], VarOrIndi, Int)]
results, offsetValue :: Int
offsetValue) arg :: DataArg
arg -> do
                result :: ([SENTENCE], VarOrIndi, Int)
result@(_, _, offsetValue' :: Int
offsetValue') <- Int -> DataArg -> Result ([SENTENCE], VarOrIndi, Int)
dArgToVarOrIndi Int
offsetValue DataArg
arg
                ([([SENTENCE], VarOrIndi, Int)], Int)
-> Result ([([SENTENCE], VarOrIndi, Int)], Int)
forall (m :: * -> *) a. Monad m => a -> m a
return (([SENTENCE], VarOrIndi, Int)
result ([SENTENCE], VarOrIndi, Int)
-> [([SENTENCE], VarOrIndi, Int)] -> [([SENTENCE], VarOrIndi, Int)]
forall a. a -> [a] -> [a]
: [([SENTENCE], VarOrIndi, Int)]
results, Int
offsetValue')
            ) ([], Int
startVar) [DataArg]
args
        let sentences :: [SENTENCE]
sentences = [[SENTENCE]] -> [SENTENCE]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[SENTENCE]] -> [SENTENCE]) -> [[SENTENCE]] -> [SENTENCE]
forall a b. (a -> b) -> a -> b
$ (([SENTENCE], VarOrIndi, Int) -> [SENTENCE])
-> [([SENTENCE], VarOrIndi, Int)] -> [[SENTENCE]]
forall a b. (a -> b) -> [a] -> [b]
map (\(s :: [SENTENCE]
s, _, _) -> [SENTENCE]
s) [([SENTENCE], VarOrIndi, Int)]
l
        let vars :: [VarOrIndi]
vars = (([SENTENCE], VarOrIndi, Int) -> VarOrIndi)
-> [([SENTENCE], VarOrIndi, Int)] -> [VarOrIndi]
forall a b. (a -> b) -> [a] -> [b]
map (\(_, v :: VarOrIndi
v, _) -> VarOrIndi
v) [([SENTENCE], VarOrIndi, Int)]
l
        let sen :: SENTENCE
sen = Token -> [TERM] -> SENTENCE
mkTermAtoms (IRI -> Token
uriToTok IRI
iri) ([TERM] -> SENTENCE) -> [TERM] -> SENTENCE
forall a b. (a -> b) -> a -> b
$ (VarOrIndi -> TERM) -> [VarOrIndi] -> [TERM]
forall a b. (a -> b) -> [a] -> [b]
map VarOrIndi -> TERM
mkVTerm [VarOrIndi]
vars
        ([SENTENCE], Sign, Int) -> Result ([SENTENCE], Sign, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return (SENTENCE
senSENTENCE -> [SENTENCE] -> [SENTENCE]
forall a. a -> [a] -> [a]
:[SENTENCE]
sentences, Sign
cSig, Int
offsetValue)

    SameIndividualAtom iarg1 :: IndividualArg
iarg1 iarg2 :: IndividualArg
iarg2 -> do
            [SENTENCE]
sens <- Sign -> SameOrDifferent -> Maybe IRI -> [IRI] -> Result [SENTENCE]
mapComIndivList Sign
cSig 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]
            ([SENTENCE], Sign, Int) -> Result ([SENTENCE], Sign, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ([SENTENCE]
sens, Sign
cSig, Int
startVar)
        
    DifferentIndividualsAtom iarg1 :: IndividualArg
iarg1 iarg2 :: IndividualArg
iarg2 -> do
            [SENTENCE]
sens <- Sign -> SameOrDifferent -> Maybe IRI -> [IRI] -> Result [SENTENCE]
mapComIndivList Sign
cSig 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]
            ([SENTENCE], Sign, Int) -> Result ([SENTENCE], Sign, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ([SENTENCE]
sens, Sign
cSig, Int
startVar)
    _ -> String -> Result ([SENTENCE], Sign, Int)
forall a. HasCallStack => String -> a
error (String -> Result ([SENTENCE], Sign, Int))
-> String -> Result ([SENTENCE], Sign, Int)
forall a b. (a -> b) -> a -> b
$ "atomToSentence: 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]
++ "'!"


-- helper function
addMrs :: TEXT -> TEXT_META
addMrs :: TEXT -> TEXT_META
addMrs t :: TEXT
t = TEXT_META
emptyTextMeta { getText :: TEXT
getText = TEXT
t }