{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}
{- |
Module      :  ./OWL2/CASL2OWL.hs
Description :  Comorphism from CASL to OWL2
Copyright   :  (c) C. Maeder, DFKI GmbH 2012
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  Christian.Maeder@dfki.de
Stability   :  provisional
Portability :  non-portable (via Logic.Logic)
-}

module OWL2.CASL2OWL where

import Logic.Logic as Logic
import Logic.Comorphism

import Common.AS_Annotation
import Common.DocUtils
import Common.Result
import Common.Id
import Common.ProofTree
import Common.Utils
import qualified Common.Lib.MapSet as MapSet
import qualified Control.Monad.Fail as Fail

import qualified Data.Set as Set
import qualified Data.Map as Map
import Data.List
import Data.Maybe

-- OWL = codomain
import OWL2.Logic_OWL2
import OWL2.AS
import Common.IRI
import OWL2.ProfilesAndSublogics
import OWL2.ManchesterPrint ()
import OWL2.Morphism
import OWL2.Symbols
import OWL2.Sign as OS
import OWL2.Translate

-- CASL = domain
import CASL.Logic_CASL
import CASL.AS_Basic_CASL
import CASL.Disambiguate
import CASL.Sign as CS
import qualified CASL.MapSentence as MapSen
import CASL.Morphism
import CASL.SimplifySen
import CASL.Sublogic
import CASL.ToDoc
import CASL.Overload

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

instance Language CASL2OWL

instance Comorphism
    CASL2OWL        -- comorphism
    CASL            -- lid domain
    CASL_Sublogics  -- sublogics domain
    CASLBasicSpec   -- Basic spec domain
    CASLFORMULA     -- sentence domain
    SYMB_ITEMS      -- symbol items domain
    SYMB_MAP_ITEMS  -- symbol map items domain
    CASLSign        -- signature domain
    CASLMor         -- morphism domain
    Symbol          -- symbol domain
    RawSymbol       -- rawsymbol domain
    ProofTree       -- proof tree domain
    OWL2            -- lid codomain
    ProfSub         -- sublogics codomain
    OntologyDocument -- Basic spec codomain
    Axiom           -- sentence codomain
    SymbItems       -- symbol items codomain
    SymbMapItems    -- symbol map items codomain
    OS.Sign         -- signature codomain
    OWLMorphism     -- morphism codomain
    Entity          -- symbol codomain
    RawSymb         -- rawsymbol codomain
    ProofTree       -- proof tree codomain
    where
      sourceLogic :: CASL2OWL -> CASL
sourceLogic CASL2OWL = CASL
CASL
      sourceSublogic :: CASL2OWL -> CASL_Sublogics
sourceSublogic CASL2OWL = CASL_Sublogics
forall a. Lattice a => CASL_SL a
caslTop
        { sub_features :: SubsortingFeatures
sub_features = SubsortingFeatures
LocFilSub }
      targetLogic :: CASL2OWL -> OWL2
targetLogic CASL2OWL = OWL2
OWL2
      mapSublogic :: CASL2OWL -> CASL_Sublogics -> Maybe ProfSub
mapSublogic CASL2OWL _ = ProfSub -> Maybe ProfSub
forall a. a -> Maybe a
Just ProfSub
topS
      map_theory :: CASL2OWL
-> (CASLSign, [Named CASLFORMULA]) -> Result (Sign, [Named Axiom])
map_theory CASL2OWL = (CASLSign, [Named CASLFORMULA]) -> Result (Sign, [Named Axiom])
forall f e.
(FormExtension f, TermExtension f) =>
(Sign f e, [Named (FORMULA f)]) -> Result (Sign, [Named Axiom])
mapTheory

{- names must be disambiguated as is done in CASL.Qualify or SuleCFOL2SoftFOL.
   Ops or preds in the overload relation denote the same objectProperty!
-}

toC :: Id -> ClassExpression
toC :: Id -> ClassExpression
toC = Class -> ClassExpression
Expression (Class -> ClassExpression)
-> (Id -> Class) -> Id -> ClassExpression
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Id -> Class
idToIRI

toO :: Id -> Int -> ObjectPropertyExpression
toO :: Id -> Int -> ObjectPropertyExpression
toO i :: Id
i = Class -> ObjectPropertyExpression
ObjectProp (Class -> ObjectPropertyExpression)
-> (Int -> Class) -> Int -> ObjectPropertyExpression
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Id -> Int -> Class
idToNumberedIRI Id
i

mkObjEnt :: String -> Id -> Int -> String -> Axiom -> Named Axiom
mkObjEnt :: String -> Id -> Int -> String -> Axiom -> Named Axiom
mkObjEnt s :: String
s i :: Id
i n :: Int
n m :: String
m = String -> Axiom -> Named Axiom
forall a s. a -> s -> SenAttr s a
makeNamed (String
s String -> ShowS
forall a. [a] -> [a] -> [a]
++ Id -> String
forall a. Show a => a -> String
show Id
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ (if Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< 0 then "" else '_' Char -> ShowS
forall a. a -> [a] -> [a]
: Int -> String
forall a. Show a => a -> String
show Int
n) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
m)

toSubClass :: Id -> [ClassExpression] -> [Axiom]
toSubClass :: Id -> [ClassExpression] -> [Axiom]
toSubClass i :: Id
i = (ClassExpression -> Axiom) -> [ClassExpression] -> [Axiom]
forall a b. (a -> b) -> [a] -> [b]
map (ClassAxiom -> Axiom
ClassAxiom (ClassAxiom -> Axiom)
-> (ClassExpression -> ClassAxiom) -> ClassExpression -> Axiom
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AxiomAnnotations
-> ClassExpression -> ClassExpression -> ClassAxiom
SubClassOf [] (Id -> ClassExpression
toC Id
i))

getPropSens :: Id -> [SORT] -> Maybe SORT -> [Named Axiom]
getPropSens :: Id -> [Id] -> Maybe Id -> [Named Axiom]
getPropSens i :: Id
i args :: [Id]
args mres :: Maybe Id
mres = let
  ncs :: [(Id, Int)]
ncs = [Id] -> [(Id, Int)]
forall a. [a] -> [(a, Int)]
number [Id]
args
  opOrPred :: String
opOrPred = if Maybe Id -> Bool
forall a. Maybe a -> Bool
isJust Maybe Id
mres then "op " else "pred "
  in (Axiom -> Named Axiom) -> [Axiom] -> [Named Axiom]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (String -> Axiom -> Named Axiom
forall a s. a -> s -> SenAttr s a
makeNamed (String
opOrPred String -> ShowS
forall a. [a] -> [a] -> [a]
++ Id -> String
forall a. Show a => a -> String
show Id
i))
         (Id -> [ClassExpression] -> [Axiom]
toSubClass Id
i [JunctionType -> [ClassExpression] -> ClassExpression
ObjectJunction JunctionType
IntersectionOf
            ([ClassExpression] -> ClassExpression)
-> [ClassExpression] -> ClassExpression
forall a b. (a -> b) -> a -> b
$ Maybe ClassExpression -> [ClassExpression]
forall a. Maybe a -> [a]
maybeToList ((Id -> ClassExpression) -> Maybe Id -> Maybe ClassExpression
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Id -> ClassExpression
toC Maybe Id
mres)
            [ClassExpression] -> [ClassExpression] -> [ClassExpression]
forall a. [a] -> [a] -> [a]
++ ((Id, Int) -> ClassExpression) -> [(Id, Int)] -> [ClassExpression]
forall a b. (a -> b) -> [a] -> [b]
map (\ (a :: Id
a, n :: Int
n) -> QuantifierType
-> ObjectPropertyExpression -> ClassExpression -> ClassExpression
ObjectValuesFrom QuantifierType
SomeValuesFrom
                 (Id -> Int -> ObjectPropertyExpression
toO Id
i Int
n) (ClassExpression -> ClassExpression)
-> ClassExpression -> ClassExpression
forall a b. (a -> b) -> a -> b
$ Id -> ClassExpression
toC Id
a) [(Id, Int)]
ncs])
  [Named Axiom] -> [Named Axiom] -> [Named Axiom]
forall a. [a] -> [a] -> [a]
++ ((Id, Int) -> [Named Axiom]) -> [(Id, Int)] -> [Named Axiom]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\ (a :: Id
a, n :: Int
n) -> let mki :: String -> Axiom -> Named Axiom
mki = String -> Id -> Int -> String -> Axiom -> Named Axiom
mkObjEnt String
opOrPred Id
i Int
n in
      Maybe (Named Axiom) -> [Named Axiom]
forall a. Maybe a -> [a]
maybeToList ((Id -> Named Axiom) -> Maybe Id -> Maybe (Named Axiom)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (String -> Axiom -> Named Axiom
mki " domain" (Axiom -> Named Axiom) -> (Id -> Axiom) -> Id -> Named Axiom
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ObjectPropertyAxiom -> Axiom
ObjectPropertyAxiom (ObjectPropertyAxiom -> Axiom)
-> (Id -> ObjectPropertyAxiom) -> Id -> Axiom
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AxiomAnnotations
-> ObjectPropertyExpression
-> ClassExpression
-> ObjectPropertyAxiom
ObjectPropertyDomain [] (Id -> Int -> ObjectPropertyExpression
toO Id
i Int
n) (ClassExpression -> ObjectPropertyAxiom)
-> (Id -> ClassExpression) -> Id -> ObjectPropertyAxiom
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Id -> ClassExpression
toC) Maybe Id
mres) [Named Axiom] -> [Named Axiom] -> [Named Axiom]
forall a. [a] -> [a] -> [a]
++
      [String -> Axiom -> Named Axiom
mki " range" (Axiom -> Named Axiom) -> Axiom -> Named Axiom
forall a b. (a -> b) -> a -> b
$ ObjectPropertyAxiom -> Axiom
ObjectPropertyAxiom (ObjectPropertyAxiom -> Axiom) -> ObjectPropertyAxiom -> Axiom
forall a b. (a -> b) -> a -> b
$ AxiomAnnotations
-> ObjectPropertyExpression
-> ClassExpression
-> ObjectPropertyAxiom
ObjectPropertyRange [] (Id -> Int -> ObjectPropertyExpression
toO Id
i Int
n) (Id -> ClassExpression
toC Id
a)]) [(Id, Int)]
ncs

getPropNames :: (a -> [b]) -> MapSet.MapSet Id a -> Set.Set IRI
getPropNames :: (a -> [b]) -> MapSet Id a -> Set Class
getPropNames f :: a -> [b]
f = (Id -> Set a -> Set Class -> Set Class)
-> Set Class -> Map Id (Set a) -> Set Class
forall k a b. (k -> a -> b -> b) -> b -> Map k a -> b
Map.foldrWithKey (\ i :: Id
i s :: Set a
s l :: Set Class
l ->
    case Set a -> [a]
forall a. Set a -> [a]
Set.toList Set a
s of
      [] -> Set Class
l
      h :: a
h : _ -> Set Class -> Set Class -> Set Class
forall a. Ord a => Set a -> Set a -> Set a
Set.union Set Class
l (Set Class -> Set Class) -> Set Class -> Set Class
forall a b. (a -> b) -> a -> b
$ [Class] -> Set Class
forall a. Ord a => [a] -> Set a
Set.fromList
        ([Class] -> Set Class) -> [Class] -> Set Class
forall a b. (a -> b) -> a -> b
$ ((b, Int) -> Class) -> [(b, Int)] -> [Class]
forall a b. (a -> b) -> [a] -> [b]
map (Id -> Int -> Class
idToNumberedIRI Id
i (Int -> Class) -> ((b, Int) -> Int) -> (b, Int) -> Class
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (b, Int) -> Int
forall a b. (a, b) -> b
snd) ([(b, Int)] -> [Class]) -> [(b, Int)] -> [Class]
forall a b. (a -> b) -> a -> b
$ [b] -> [(b, Int)]
forall a. [a] -> [(a, Int)]
number ([b] -> [(b, Int)]) -> [b] -> [(b, Int)]
forall a b. (a -> b) -> a -> b
$ a -> [b]
f a
h)
    Set Class
forall a. Set a
Set.empty (Map Id (Set a) -> Set Class)
-> (MapSet Id a -> Map Id (Set a)) -> MapSet Id a -> Set Class
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MapSet Id a -> Map Id (Set a)
forall a b. MapSet a b -> Map a (Set b)
MapSet.toMap

commonType :: CS.Sign f e -> [[SORT]] -> Result [SORT]
commonType :: Sign f e -> [[Id]] -> Result [Id]
commonType csig :: Sign f e
csig l :: [[Id]]
l =
  case ([Id] -> [Id]) -> [[Id]] -> [[Id]]
forall a b. (a -> b) -> [a] -> [b]
map (Sign f e -> [Id] -> [Id]
forall f e. Sign f e -> [Id] -> [Id]
keepMaximals Sign f e
csig) ([[Id]] -> [[Id]]) -> [[Id]] -> [[Id]]
forall a b. (a -> b) -> a -> b
$ [[Id]] -> [[Id]]
forall a. [[a]] -> [[a]]
transpose [[Id]]
l of
    hl :: [[Id]]
hl | ([Id] -> Bool) -> [[Id]] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Bool -> Bool
not (Bool -> Bool) -> ([Id] -> Bool) -> [Id] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Id] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null) [[Id]]
hl -> [Id] -> Result [Id]
forall (m :: * -> *) a. Monad m => a -> m a
return ([Id] -> Result [Id]) -> [Id] -> Result [Id]
forall a b. (a -> b) -> a -> b
$ ([Id] -> Id) -> [[Id]] -> [Id]
forall a b. (a -> b) -> [a] -> [b]
map [Id] -> Id
forall a. [a] -> a
head [[Id]]
hl
    _ -> String -> Result [Id]
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail (String -> Result [Id]) -> String -> Result [Id]
forall a b. (a -> b) -> a -> b
$ "no common types for " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [[Id]] -> String
forall a. Show a => a -> String
show [[Id]]
l

commonOpType :: CS.Sign f e -> Set.Set OpType -> Result OpType
commonOpType :: Sign f e -> Set OpType -> Result OpType
commonOpType csig :: Sign f e
csig os :: Set OpType
os = do
  [Id]
l <- Sign f e -> [[Id]] -> Result [Id]
forall f e. Sign f e -> [[Id]] -> Result [Id]
commonType Sign f e
csig ([[Id]] -> Result [Id]) -> [[Id]] -> Result [Id]
forall a b. (a -> b) -> a -> b
$ (OpType -> [Id]) -> [OpType] -> [[Id]]
forall a b. (a -> b) -> [a] -> [b]
map (\ o :: OpType
o -> OpType -> Id
opRes OpType
o Id -> [Id] -> [Id]
forall a. a -> [a] -> [a]
: OpType -> [Id]
opArgs OpType
o) ([OpType] -> [[Id]]) -> [OpType] -> [[Id]]
forall a b. (a -> b) -> a -> b
$ Set OpType -> [OpType]
forall a. Set a -> [a]
Set.toList Set OpType
os
  case [Id]
l of
    r :: Id
r : args :: [Id]
args -> OpType -> Result OpType
forall (m :: * -> *) a. Monad m => a -> m a
return (OpType -> Result OpType) -> OpType -> Result OpType
forall a b. (a -> b) -> a -> b
$ [Id] -> Id -> OpType
mkTotOpType [Id]
args Id
r
    _ -> String -> Result OpType
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail (String -> Result OpType) -> String -> Result OpType
forall a b. (a -> b) -> a -> b
$ "no common types for " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Set OpType -> ShowS
forall a. Pretty a => a -> ShowS
showDoc Set OpType
os ""

commonPredType :: CS.Sign f e -> Set.Set PredType -> Result PredType
commonPredType :: Sign f e -> Set PredType -> Result PredType
commonPredType csig :: Sign f e
csig ps :: Set PredType
ps = do
  [Id]
args <- Sign f e -> [[Id]] -> Result [Id]
forall f e. Sign f e -> [[Id]] -> Result [Id]
commonType Sign f e
csig ([[Id]] -> Result [Id]) -> [[Id]] -> Result [Id]
forall a b. (a -> b) -> a -> b
$ (PredType -> [Id]) -> [PredType] -> [[Id]]
forall a b. (a -> b) -> [a] -> [b]
map PredType -> [Id]
predArgs ([PredType] -> [[Id]]) -> [PredType] -> [[Id]]
forall a b. (a -> b) -> a -> b
$ Set PredType -> [PredType]
forall a. Set a -> [a]
Set.toList Set PredType
ps
  case [Id]
args of
    _ : _ -> PredType -> Result PredType
forall (m :: * -> *) a. Monad m => a -> m a
return (PredType -> Result PredType) -> PredType -> Result PredType
forall a b. (a -> b) -> a -> b
$ [Id] -> PredType
PredType [Id]
args
    _ -> String -> Result PredType
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail (String -> Result PredType) -> String -> Result PredType
forall a b. (a -> b) -> a -> b
$ "no common types for " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Set PredType -> ShowS
forall a. Pretty a => a -> ShowS
showDoc Set PredType
ps ""

getCommonSupers :: CS.Sign f e -> [SORT] -> Set.Set SORT
getCommonSupers :: Sign f e -> [Id] -> Set Id
getCommonSupers csig :: Sign f e
csig s :: [Id]
s = let supers :: Id -> Set Id
supers t :: Id
t = Id -> Set Id -> Set Id
forall a. Ord a => a -> Set a -> Set a
Set.insert Id
t (Set Id -> Set Id) -> Set Id -> Set Id
forall a b. (a -> b) -> a -> b
$ Id -> Sign f e -> Set Id
forall f e. Id -> Sign f e -> Set Id
supersortsOf Id
t Sign f e
csig in
   if [Id] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Id]
s then Set Id
forall a. Set a
Set.empty else (Set Id -> Set Id -> Set Id) -> [Set Id] -> Set Id
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 Set Id -> Set Id -> Set Id
forall a. Ord a => Set a -> Set a -> Set a
Set.intersection ([Set Id] -> Set Id) -> [Set Id] -> Set Id
forall a b. (a -> b) -> a -> b
$ (Id -> Set Id) -> [Id] -> [Set Id]
forall a b. (a -> b) -> [a] -> [b]
map Id -> Set Id
supers [Id]
s

keepMaximals :: CS.Sign f e -> [SORT] -> [SORT]
keepMaximals :: Sign f e -> [Id] -> [Id]
keepMaximals csig :: Sign f e
csig = Bool -> Sign f e -> (Id -> Id) -> [Id] -> [Id]
forall f e a. Bool -> Sign f e -> (a -> Id) -> [a] -> [a]
keepMinimals1 Bool
True Sign f e
csig Id -> Id
forall a. a -> a
id ([Id] -> [Id]) -> ([Id] -> [Id]) -> [Id] -> [Id]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set Id -> [Id]
forall a. Set a -> [a]
Set.toList
  (Set Id -> [Id]) -> ([Id] -> Set Id) -> [Id] -> [Id]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sign f e -> [Id] -> Set Id
forall f e. Sign f e -> [Id] -> Set Id
getCommonSupers Sign f e
csig

mapSign :: CS.Sign f e -> Result (OS.Sign, [Named Axiom])
mapSign :: Sign f e -> Result (Sign, [Named Axiom])
mapSign csig :: Sign f e
csig = let
  esorts :: Set Id
esorts = Sign f e -> Set Id
forall f e. Sign f e -> Set Id
emptySortSet Sign f e
csig
  srel :: Rel Id
srel = Sign f e -> Rel Id
forall f e. Sign f e -> Rel Id
sortRel Sign f e
csig
  (eqs :: [[Id]]
eqs, subss :: [(Id, [Id])]
subss) = Bool -> Rel Id -> ([[Id]], [(Id, [Id])])
eqAndSubsorts Bool
False Rel Id
srel
  (isos :: [Id]
isos, rels :: [[Id]]
rels) = Rel Id -> ([Id], [[Id]])
singleAndRelatedSorts Rel Id
srel
  ss :: Set Id
ss = Sign f e -> Set Id
forall f e. Sign f e -> Set Id
sortSet Sign f e
csig
  nsorts :: Set Id
nsorts = Set Id -> Set Id -> Set Id
forall a. Ord a => Set a -> Set a -> Set a
Set.difference Set Id
ss Set Id
esorts
  mkDisjC :: [Id] -> Axiom
mkDisjC l :: [Id]
l = ClassAxiom -> Axiom
ClassAxiom (ClassAxiom -> Axiom) -> ClassAxiom -> Axiom
forall a b. (a -> b) -> a -> b
$ AxiomAnnotations -> [ClassExpression] -> ClassAxiom
DisjointClasses [] ([ClassExpression] -> ClassAxiom)
-> [ClassExpression] -> ClassAxiom
forall a b. (a -> b) -> a -> b
$ (Id -> ClassExpression) -> [Id] -> [ClassExpression]
forall a b. (a -> b) -> [a] -> [b]
map Id -> ClassExpression
toC [Id]
l
  mkEqivC :: [Id] -> Axiom
mkEqivC l :: [Id]
l = ClassAxiom -> Axiom
ClassAxiom (ClassAxiom -> Axiom) -> ClassAxiom -> Axiom
forall a b. (a -> b) -> a -> b
$ AxiomAnnotations -> [ClassExpression] -> ClassAxiom
EquivalentClasses [] ([ClassExpression] -> ClassAxiom)
-> [ClassExpression] -> ClassAxiom
forall a b. (a -> b) -> a -> b
$ (Id -> ClassExpression) -> [Id] -> [ClassExpression]
forall a b. (a -> b) -> [a] -> [b]
map Id -> ClassExpression
toC [Id]
l
  disjSorts :: [Named Axiom]
disjSorts = ([Id] -> [Named Axiom]) -> [[Id]] -> [Named Axiom]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\ l :: [Id]
l -> case [Id]
l of
    _ : _ : _ -> [String -> Axiom -> Named Axiom
forall a s. a -> s -> SenAttr s a
makeNamed ("disjoint " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [Id] -> String
forall a. Show a => a -> String
show [Id]
l) (Axiom -> Named Axiom) -> Axiom -> Named Axiom
forall a b. (a -> b) -> a -> b
$ [Id] -> Axiom
mkDisjC [Id]
l]
    _ -> []) ([[Id]] -> [Named Axiom])
-> ([[Id]] -> [[Id]]) -> [[Id]] -> [Named Axiom]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [[Id]] -> [[Id]]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence ([[Id]] -> [Named Axiom]) -> [[Id]] -> [Named Axiom]
forall a b. (a -> b) -> a -> b
$ (Id -> [Id]) -> [Id] -> [[Id]]
forall a b. (a -> b) -> [a] -> [b]
map (Id -> [Id] -> [Id]
forall a. a -> [a] -> [a]
: []) [Id]
isos [[Id]] -> [[Id]] -> [[Id]]
forall a. [a] -> [a] -> [a]
++ ([Id] -> [Id]) -> [[Id]] -> [[Id]]
forall a b. (a -> b) -> [a] -> [b]
map (Sign f e -> [Id] -> [Id]
forall f e. Sign f e -> [Id] -> [Id]
keepMaximals Sign f e
csig) [[Id]]
rels
  eqSorts :: [Named Axiom]
eqSorts = ([Id] -> Named Axiom) -> [[Id]] -> [Named Axiom]
forall a b. (a -> b) -> [a] -> [b]
map (\ es :: [Id]
es -> String -> Axiom -> Named Axiom
forall a s. a -> s -> SenAttr s a
makeNamed ("equal sorts " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [Id] -> String
forall a. Show a => a -> String
show [Id]
es)
                 (Axiom -> Named Axiom) -> Axiom -> Named Axiom
forall a b. (a -> b) -> a -> b
$ [Id] -> Axiom
mkEqivC [Id]
es) [[Id]]
eqs
  subSens :: [Named Axiom]
subSens = ((Id, [Id]) -> [Named Axiom]) -> [(Id, [Id])] -> [Named Axiom]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\ (s :: Id
s, ts :: [Id]
ts) -> String -> Axiom -> Named Axiom
forall a s. a -> s -> SenAttr s a
makeNamed
    ("subsort " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Id -> String
forall a. Show a => a -> String
show Id
s String -> ShowS
forall a. [a] -> [a] -> [a]
++ " of " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [Id] -> String
forall a. Show a => a -> String
show [Id]
ts) (Axiom -> Named Axiom) -> [Axiom] -> [Named Axiom]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Id -> [Id] -> [Axiom]
toSC Id
s [Id]
ts) [(Id, [Id])]
subss
  nonEmptySens :: [Named Axiom]
nonEmptySens = (Id -> [Named Axiom]) -> [Id] -> [Named Axiom]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\ s :: Id
s -> Bool -> Id -> [Id] -> [Named Axiom]
mkIndi Bool
True Id
s [Id
s]) ([Id] -> [Named Axiom]) -> [Id] -> [Named Axiom]
forall a b. (a -> b) -> a -> b
$ Set Id -> [Id]
forall a. Set a -> [a]
Set.toList Set Id
nsorts
  sortSens :: [Named Axiom]
sortSens = [Named Axiom]
eqSorts [Named Axiom] -> [Named Axiom] -> [Named Axiom]
forall a. [a] -> [a] -> [a]
++ [Named Axiom]
disjSorts [Named Axiom] -> [Named Axiom] -> [Named Axiom]
forall a. [a] -> [a] -> [a]
++ [Named Axiom]
subSens [Named Axiom] -> [Named Axiom] -> [Named Axiom]
forall a. [a] -> [a] -> [a]
++ [Named Axiom]
nonEmptySens
  mkIndi :: Bool -> Id -> [Id] -> [Named Axiom]
mkIndi b :: Bool
b i :: Id
i ts :: [Id]
ts = String -> Axiom -> Named Axiom
forall a s. a -> s -> SenAttr s a
makeNamed
        ("individual " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Id -> String
forall a. Show a => a -> String
show Id
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ " of class " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [Id] -> ShowS
forall a. Pretty a => a -> ShowS
showDoc [Id]
ts "")
        (Axiom -> Named Axiom) -> [Axiom] -> [Named Axiom]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Id -> Axiom) -> [Id] -> [Axiom]
forall a b. (a -> b) -> [a] -> [b]
map (\t :: Id
t -> Assertion -> Axiom
Assertion (Assertion -> Axiom) -> Assertion -> Axiom
forall a b. (a -> b) -> a -> b
$ AxiomAnnotations -> ClassExpression -> Class -> Assertion
ClassAssertion [] (Id -> ClassExpression
toC Id
t) (Bool -> Id -> Class
idToAnonIRI Bool
b Id
i)) [Id]
ts
  om :: OpMap
om = Sign f e -> OpMap
forall f e. Sign f e -> OpMap
opMap Sign f e
csig
  keepMaxs :: [Id] -> [Id]
keepMaxs = Sign f e -> [Id] -> [Id]
forall f e. Sign f e -> [Id] -> [Id]
keepMaximals Sign f e
csig
  mk :: String -> Id -> String -> Axiom -> Named Axiom
mk s :: String
s i :: Id
i = String -> Id -> Int -> String -> Axiom -> Named Axiom
mkObjEnt String
s Id
i (-1)
  toSC :: Id -> [Id] -> [Axiom]
toSC i :: Id
i = Id -> [ClassExpression] -> [Axiom]
toSubClass Id
i ([ClassExpression] -> [Axiom])
-> ([Id] -> [ClassExpression]) -> [Id] -> [Axiom]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Id -> ClassExpression) -> [Id] -> [ClassExpression]
forall a b. (a -> b) -> [a] -> [b]
map Id -> ClassExpression
toC
  toIris :: Set Id -> Set Class
toIris = (Id -> Class) -> Set Id -> Set Class
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map Id -> Class
idToIRI
  (cs :: OpMap
cs, ncs :: OpMap
ncs) = (OpType -> Bool) -> OpMap -> (OpMap, OpMap)
forall a b.
(Ord a, Ord b) =>
(b -> Bool) -> MapSet a b -> (MapSet a b, MapSet a b)
MapSet.partition ([Id] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([Id] -> Bool) -> (OpType -> [Id]) -> OpType -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. OpType -> [Id]
opArgs) OpMap
om
  (sos :: OpMap
sos, os :: OpMap
os) = (OpType -> Bool) -> OpMap -> (OpMap, OpMap)
forall a b.
(Ord a, Ord b) =>
(b -> Bool) -> MapSet a b -> (MapSet a b, MapSet a b)
MapSet.partition OpType -> Bool
isSingleArgOp OpMap
ncs
  (props :: MapSet Id PredType
props, nps :: MapSet Id PredType
nps) = (PredType -> Bool)
-> MapSet Id PredType -> (MapSet Id PredType, MapSet Id PredType)
forall a b.
(Ord a, Ord b) =>
(b -> Bool) -> MapSet a b -> (MapSet a b, MapSet a b)
MapSet.partition ([Id] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([Id] -> Bool) -> (PredType -> [Id]) -> PredType -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PredType -> [Id]
predArgs) MapSet Id PredType
pm
  (sps :: MapSet Id PredType
sps, rps' :: MapSet Id PredType
rps') = (PredType -> Bool)
-> MapSet Id PredType -> (MapSet Id PredType, MapSet Id PredType)
forall a b.
(Ord a, Ord b) =>
(b -> Bool) -> MapSet a b -> (MapSet a b, MapSet a b)
MapSet.partition ([Id] -> Bool
forall a. [a] -> Bool
isSingle ([Id] -> Bool) -> (PredType -> [Id]) -> PredType -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PredType -> [Id]
predArgs) MapSet Id PredType
nps
  (bps :: MapSet Id PredType
bps, ps :: MapSet Id PredType
ps) = (PredType -> Bool)
-> MapSet Id PredType -> (MapSet Id PredType, MapSet Id PredType)
forall a b.
(Ord a, Ord b) =>
(b -> Bool) -> MapSet a b -> (MapSet a b, MapSet a b)
MapSet.partition PredType -> Bool
isBinPredType MapSet Id PredType
rps'
  pm :: MapSet Id PredType
pm = Sign f e -> MapSet Id PredType
forall f e. Sign f e -> MapSet Id PredType
predMap Sign f e
csig
  osig :: Sign
osig = Sign
OS.emptySign
    { concepts :: Set Class
concepts = Set Id -> Set Class
toIris (Set Id -> Set Class) -> Set Id -> Set Class
forall a b. (a -> b) -> a -> b
$ [Set Id] -> Set Id
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions
      [ Set Id
ss, MapSet Id PredType -> Set Id
forall a b. MapSet a b -> Set a
MapSet.keysSet MapSet Id PredType
sps, MapSet Id PredType -> Set Id
forall a b. MapSet a b -> Set a
MapSet.keysSet MapSet Id PredType
props
      , OpMap -> Set Id
forall a b. MapSet a b -> Set a
MapSet.keysSet OpMap
os, MapSet Id PredType -> Set Id
forall a b. MapSet a b -> Set a
MapSet.keysSet MapSet Id PredType
ps]
    , objectProperties :: Set Class
objectProperties = [Set Class] -> Set Class
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions
      [ Set Id -> Set Class
toIris (Set Id -> Set Class) -> Set Id -> Set Class
forall a b. (a -> b) -> a -> b
$ Set Id -> Set Id -> Set Id
forall a. Ord a => Set a -> Set a -> Set a
Set.union (OpMap -> Set Id
forall a b. MapSet a b -> Set a
MapSet.keysSet OpMap
sos) (Set Id -> Set Id) -> Set Id -> Set Id
forall a b. (a -> b) -> a -> b
$ MapSet Id PredType -> Set Id
forall a b. MapSet a b -> Set a
MapSet.keysSet MapSet Id PredType
bps
      , (PredType -> [Id]) -> MapSet Id PredType -> Set Class
forall a b. (a -> [b]) -> MapSet Id a -> Set Class
getPropNames PredType -> [Id]
predArgs MapSet Id PredType
ps, (OpType -> [Id]) -> OpMap -> Set Class
forall a b. (a -> [b]) -> MapSet Id a -> Set Class
getPropNames OpType -> [Id]
opArgs OpMap
os ]
    , individuals :: Set Class
individuals = Set Id -> Set Class
toIris (Set Id -> Set Class) -> Set Id -> Set Class
forall a b. (a -> b) -> a -> b
$ OpMap -> Set Id
forall a b. MapSet a b -> Set a
MapSet.keysSet OpMap
cs
    }
  in do
  [Named Axiom]
s1 <- (Id -> Set OpType -> Result [Named Axiom] -> Result [Named Axiom])
-> Result [Named Axiom]
-> Map Id (Set OpType)
-> Result [Named Axiom]
forall k a b. (k -> a -> b -> b) -> b -> Map k a -> b
Map.foldrWithKey (\ i :: Id
i s :: Set OpType
s ml :: Result [Named Axiom]
ml -> do
      [Named Axiom]
l <- Result [Named Axiom]
ml
      [Named Axiom] -> Result [Named Axiom]
forall (m :: * -> *) a. Monad m => a -> m a
return ([Named Axiom] -> Result [Named Axiom])
-> [Named Axiom] -> Result [Named Axiom]
forall a b. (a -> b) -> a -> b
$ Bool -> Id -> [Id] -> [Named Axiom]
mkIndi Bool
False Id
i
        (Sign f e -> (Id -> Id) -> [Id] -> [Id]
forall f e a. Sign f e -> (a -> Id) -> [a] -> [a]
keepMinimals Sign f e
csig Id -> Id
forall a. a -> a
id ([Id] -> [Id]) -> [Id] -> [Id]
forall a b. (a -> b) -> a -> b
$ (OpType -> Id) -> [OpType] -> [Id]
forall a b. (a -> b) -> [a] -> [b]
map OpType -> Id
opRes ([OpType] -> [Id]) -> [OpType] -> [Id]
forall a b. (a -> b) -> a -> b
$ Set OpType -> [OpType]
forall a. Set a -> [a]
Set.toList Set OpType
s) [Named Axiom] -> [Named Axiom] -> [Named Axiom]
forall a. [a] -> [a] -> [a]
++ [Named Axiom]
l)
    ([Named Axiom] -> Result [Named Axiom]
forall (m :: * -> *) a. Monad m => a -> m a
return [Named Axiom]
sortSens) (OpMap -> Map Id (Set OpType)
forall a b. MapSet a b -> Map a (Set b)
MapSet.toMap OpMap
cs)
  [Named Axiom]
s2 <- (Id -> Set OpType -> Result [Named Axiom] -> Result [Named Axiom])
-> Result [Named Axiom]
-> Map Id (Set OpType)
-> Result [Named Axiom]
forall k a b. (k -> a -> b -> b) -> b -> Map k a -> b
Map.foldrWithKey (\ i :: Id
i s :: Set OpType
s ml :: Result [Named Axiom]
ml -> do
    [Named Axiom]
l <- Result [Named Axiom]
ml
    let sl :: [OpType]
sl = Set OpType -> [OpType]
forall a. Set a -> [a]
Set.toList Set OpType
s
        mki :: String -> Axiom -> Named Axiom
mki = String -> Id -> String -> Axiom -> Named Axiom
mk "plain function " Id
i
        oi :: ObjectPropertyExpression
oi = Id -> Int -> ObjectPropertyExpression
toO Id
i (-1)
    case ([Id] -> [Id]
keepMaxs ([Id] -> [Id]) -> [Id] -> [Id]
forall a b. (a -> b) -> a -> b
$ (OpType -> [Id]) -> [OpType] -> [Id]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap OpType -> [Id]
opArgs [OpType]
sl, [Id] -> [Id]
keepMaxs ([Id] -> [Id]) -> [Id] -> [Id]
forall a b. (a -> b) -> a -> b
$ (OpType -> Id) -> [OpType] -> [Id]
forall a b. (a -> b) -> [a] -> [b]
map OpType -> Id
opRes [OpType]
sl) of
      ([a :: Id
a], [r :: Id
r]) -> [Named Axiom] -> Result [Named Axiom]
forall (m :: * -> *) a. Monad m => a -> m a
return
         ([Named Axiom] -> Result [Named Axiom])
-> [Named Axiom] -> Result [Named Axiom]
forall a b. (a -> b) -> a -> b
$ [ String -> Axiom -> Named Axiom
mki " character" (Axiom -> Named Axiom) -> Axiom -> Named Axiom
forall a b. (a -> b) -> a -> b
$ ObjectPropertyAxiom -> Axiom
ObjectPropertyAxiom (ObjectPropertyAxiom -> Axiom) -> ObjectPropertyAxiom -> Axiom
forall a b. (a -> b) -> a -> b
$ AxiomAnnotations -> ObjectPropertyExpression -> ObjectPropertyAxiom
FunctionalObjectProperty [] ObjectPropertyExpression
oi
           , String -> Axiom -> Named Axiom
mki " domain" (Axiom -> Named Axiom) -> Axiom -> Named Axiom
forall a b. (a -> b) -> a -> b
$ ObjectPropertyAxiom -> Axiom
ObjectPropertyAxiom (ObjectPropertyAxiom -> Axiom) -> ObjectPropertyAxiom -> Axiom
forall a b. (a -> b) -> a -> b
$ AxiomAnnotations
-> ObjectPropertyExpression
-> ClassExpression
-> ObjectPropertyAxiom
ObjectPropertyDomain [] ObjectPropertyExpression
oi (Id -> ClassExpression
toC Id
a)
           , String -> Axiom -> Named Axiom
mki " range" (Axiom -> Named Axiom) -> Axiom -> Named Axiom
forall a b. (a -> b) -> a -> b
$ ObjectPropertyAxiom -> Axiom
ObjectPropertyAxiom (ObjectPropertyAxiom -> Axiom) -> ObjectPropertyAxiom -> Axiom
forall a b. (a -> b) -> a -> b
$ AxiomAnnotations
-> ObjectPropertyExpression
-> ClassExpression
-> ObjectPropertyAxiom
ObjectPropertyRange [] ObjectPropertyExpression
oi (Id -> ClassExpression
toC Id
r)]
         [Named Axiom] -> [Named Axiom] -> [Named Axiom]
forall a. [a] -> [a] -> [a]
++ [Named Axiom]
l
      (as :: [Id]
as, rs :: [Id]
rs) -> String -> Result [Named Axiom]
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail (String -> Result [Named Axiom]) -> String -> Result [Named Axiom]
forall a b. (a -> b) -> a -> b
$ "CASL2OWL.mapSign2: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Id -> String
forall a. Show a => a -> String
show Id
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ " args: "
                   String -> ShowS
forall a. [a] -> [a] -> [a]
++ [Id] -> String
forall a. Show a => a -> String
show [Id]
as String -> ShowS
forall a. [a] -> [a] -> [a]
++ " resulttypes: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [Id] -> String
forall a. Show a => a -> String
show [Id]
rs)
    ([Named Axiom] -> Result [Named Axiom]
forall (m :: * -> *) a. Monad m => a -> m a
return [Named Axiom]
s1) (OpMap -> Map Id (Set OpType)
forall a b. MapSet a b -> Map a (Set b)
MapSet.toMap OpMap
sos)
  [Named Axiom]
s3 <- (Id
 -> Set PredType -> Result [Named Axiom] -> Result [Named Axiom])
-> Result [Named Axiom]
-> Map Id (Set PredType)
-> Result [Named Axiom]
forall k a b. (k -> a -> b -> b) -> b -> Map k a -> b
Map.foldrWithKey (\ i :: Id
i s :: Set PredType
s ml :: Result [Named Axiom]
ml -> do
    [Named Axiom]
l <- Result [Named Axiom]
ml
    let mkp :: String -> Axiom -> Named Axiom
mkp = String -> Id -> String -> Axiom -> Named Axiom
mk "binary predicate " Id
i
        oi :: ObjectPropertyExpression
oi = Id -> Int -> ObjectPropertyExpression
toO Id
i (-1)
    PredType
pTy <- Sign f e -> Set PredType -> Result PredType
forall f e. Sign f e -> Set PredType -> Result PredType
commonPredType Sign f e
csig Set PredType
s
    case PredType -> [Id]
predArgs PredType
pTy of
      [a :: Id
a, r :: Id
r] -> [Named Axiom] -> Result [Named Axiom]
forall (m :: * -> *) a. Monad m => a -> m a
return
         ([Named Axiom] -> Result [Named Axiom])
-> [Named Axiom] -> Result [Named Axiom]
forall a b. (a -> b) -> a -> b
$ [ String -> Axiom -> Named Axiom
mkp " domain" (Axiom -> Named Axiom) -> Axiom -> Named Axiom
forall a b. (a -> b) -> a -> b
$ ObjectPropertyAxiom -> Axiom
ObjectPropertyAxiom (ObjectPropertyAxiom -> Axiom) -> ObjectPropertyAxiom -> Axiom
forall a b. (a -> b) -> a -> b
$ AxiomAnnotations
-> ObjectPropertyExpression
-> ClassExpression
-> ObjectPropertyAxiom
ObjectPropertyDomain [] ObjectPropertyExpression
oi (Id -> ClassExpression
toC Id
a)
           , String -> Axiom -> Named Axiom
mkp " range" (Axiom -> Named Axiom) -> Axiom -> Named Axiom
forall a b. (a -> b) -> a -> b
$ ObjectPropertyAxiom -> Axiom
ObjectPropertyAxiom (ObjectPropertyAxiom -> Axiom) -> ObjectPropertyAxiom -> Axiom
forall a b. (a -> b) -> a -> b
$ AxiomAnnotations
-> ObjectPropertyExpression
-> ClassExpression
-> ObjectPropertyAxiom
ObjectPropertyRange [] ObjectPropertyExpression
oi (Id -> ClassExpression
toC Id
r)]
         [Named Axiom] -> [Named Axiom] -> [Named Axiom]
forall a. [a] -> [a] -> [a]
++ [Named Axiom]
l
      ts :: [Id]
ts -> String -> Result [Named Axiom]
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail (String -> Result [Named Axiom]) -> String -> Result [Named Axiom]
forall a b. (a -> b) -> a -> b
$ "CASL2OWL.mapSign3: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Id -> String
forall a. Show a => a -> String
show Id
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ " types: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [Id] -> String
forall a. Show a => a -> String
show [Id]
ts)
    ([Named Axiom] -> Result [Named Axiom]
forall (m :: * -> *) a. Monad m => a -> m a
return [Named Axiom]
s2) (MapSet Id PredType -> Map Id (Set PredType)
forall a b. MapSet a b -> Map a (Set b)
MapSet.toMap MapSet Id PredType
bps)
  [Named Axiom]
s4 <- (Id
 -> Set PredType -> Result [Named Axiom] -> Result [Named Axiom])
-> Result [Named Axiom]
-> Map Id (Set PredType)
-> Result [Named Axiom]
forall k a b. (k -> a -> b -> b) -> b -> Map k a -> b
Map.foldrWithKey (\ i :: Id
i s :: Set PredType
s ml :: Result [Named Axiom]
ml ->
     case [Id] -> [Id]
keepMaxs ([Id] -> [Id]) -> [Id] -> [Id]
forall a b. (a -> b) -> a -> b
$ (PredType -> [Id]) -> [PredType] -> [Id]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap PredType -> [Id]
predArgs ([PredType] -> [Id]) -> [PredType] -> [Id]
forall a b. (a -> b) -> a -> b
$ Set PredType -> [PredType]
forall a. Set a -> [a]
Set.toList Set PredType
s of
       [r :: Id
r] -> do
         [Named Axiom]
l <- Result [Named Axiom]
ml
         [Named Axiom] -> Result [Named Axiom]
forall (m :: * -> *) a. Monad m => a -> m a
return ([Named Axiom] -> Result [Named Axiom])
-> [Named Axiom] -> Result [Named Axiom]
forall a b. (a -> b) -> a -> b
$ (Axiom -> Named Axiom) -> [Axiom] -> [Named Axiom]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (String -> Axiom -> Named Axiom
forall a s. a -> s -> SenAttr s a
makeNamed ("plain predicate " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Id -> String
forall a. Show a => a -> String
show Id
i)) (Id -> [Id] -> [Axiom]
toSC Id
i [Id
r]) [Named Axiom] -> [Named Axiom] -> [Named Axiom]
forall a. [a] -> [a] -> [a]
++ [Named Axiom]
l
       ts :: [Id]
ts -> String -> Result [Named Axiom]
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail (String -> Result [Named Axiom]) -> String -> Result [Named Axiom]
forall a b. (a -> b) -> a -> b
$ "CASL2OWL.mapSign4: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Id -> String
forall a. Show a => a -> String
show Id
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ " types: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [Id] -> String
forall a. Show a => a -> String
show [Id]
ts)
     ([Named Axiom] -> Result [Named Axiom]
forall (m :: * -> *) a. Monad m => a -> m a
return [Named Axiom]
s3) (MapSet Id PredType -> Map Id (Set PredType)
forall a b. MapSet a b -> Map a (Set b)
MapSet.toMap MapSet Id PredType
sps)
  [Named Axiom]
s5 <- (Id -> Set OpType -> Result [Named Axiom] -> Result [Named Axiom])
-> Result [Named Axiom]
-> Map Id (Set OpType)
-> Result [Named Axiom]
forall k a b. (k -> a -> b -> b) -> b -> Map k a -> b
Map.foldrWithKey (\ i :: Id
i s :: Set OpType
s ml :: Result [Named Axiom]
ml -> do
     [Named Axiom]
l <- Result [Named Axiom]
ml
     OpType
ot <- Sign f e -> Set OpType -> Result OpType
forall f e. Sign f e -> Set OpType -> Result OpType
commonOpType Sign f e
csig Set OpType
s
     [Named Axiom] -> Result [Named Axiom]
forall (m :: * -> *) a. Monad m => a -> m a
return ([Named Axiom] -> Result [Named Axiom])
-> [Named Axiom] -> Result [Named Axiom]
forall a b. (a -> b) -> a -> b
$ Id -> [Id] -> Maybe Id -> [Named Axiom]
getPropSens Id
i (OpType -> [Id]
opArgs OpType
ot) (Id -> Maybe Id
forall a. a -> Maybe a
Just (Id -> Maybe Id) -> Id -> Maybe Id
forall a b. (a -> b) -> a -> b
$ OpType -> Id
opRes OpType
ot) [Named Axiom] -> [Named Axiom] -> [Named Axiom]
forall a. [a] -> [a] -> [a]
++ [Named Axiom]
l
     ) ([Named Axiom] -> Result [Named Axiom]
forall (m :: * -> *) a. Monad m => a -> m a
return [Named Axiom]
s4) (OpMap -> Map Id (Set OpType)
forall a b. MapSet a b -> Map a (Set b)
MapSet.toMap OpMap
os)
  [Named Axiom]
s6 <- (Id
 -> Set PredType -> Result [Named Axiom] -> Result [Named Axiom])
-> Result [Named Axiom]
-> Map Id (Set PredType)
-> Result [Named Axiom]
forall k a b. (k -> a -> b -> b) -> b -> Map k a -> b
Map.foldrWithKey (\ i :: Id
i s :: Set PredType
s ml :: Result [Named Axiom]
ml -> do
     [Named Axiom]
l <- Result [Named Axiom]
ml
     PredType
pt <- Sign f e -> Set PredType -> Result PredType
forall f e. Sign f e -> Set PredType -> Result PredType
commonPredType Sign f e
csig Set PredType
s
     [Named Axiom] -> Result [Named Axiom]
forall (m :: * -> *) a. Monad m => a -> m a
return ([Named Axiom] -> Result [Named Axiom])
-> [Named Axiom] -> Result [Named Axiom]
forall a b. (a -> b) -> a -> b
$ Id -> [Id] -> Maybe Id -> [Named Axiom]
getPropSens Id
i (PredType -> [Id]
predArgs PredType
pt) Maybe Id
forall a. Maybe a
Nothing [Named Axiom] -> [Named Axiom] -> [Named Axiom]
forall a. [a] -> [a] -> [a]
++ [Named Axiom]
l
     ) ([Named Axiom] -> Result [Named Axiom]
forall (m :: * -> *) a. Monad m => a -> m a
return [Named Axiom]
s5) (MapSet Id PredType -> Map Id (Set PredType)
forall a b. MapSet a b -> Map a (Set b)
MapSet.toMap MapSet Id PredType
ps)
  (Sign, [Named Axiom]) -> Result (Sign, [Named Axiom])
forall (m :: * -> *) a. Monad m => a -> m a
return (Sign
osig, [Named Axiom]
s6)

{- binary predicates and single argument functions should become
   objectProperties.
   Serge also turned constructors into concepts.
   How to treat multi-argument predicates and functions?
   Maybe create tuple concepts?
-}

mapTheory :: (FormExtension f, TermExtension f)
  => (CS.Sign f e, [Named (FORMULA f)]) -> Result (OS.Sign, [Named Axiom])
mapTheory :: (Sign f e, [Named (FORMULA f)]) -> Result (Sign, [Named Axiom])
mapTheory (sig :: Sign f e
sig, sens :: [Named (FORMULA f)]
sens) = do
  let mor :: Morphism f e ()
mor = Sign f e -> Morphism f e ()
forall f e. Sign f e -> Morphism f e ()
disambigSig Sign f e
sig
      tar :: Sign f e
tar = Morphism f e () -> Sign f e
forall f e m. Morphism f e m -> Sign f e
mtarget Morphism f e ()
mor
      nss :: [Named (FORMULA f)]
nss = (Named (FORMULA f) -> Named (FORMULA f))
-> [Named (FORMULA f)] -> [Named (FORMULA f)]
forall a b. (a -> b) -> [a] -> [b]
map ((FORMULA f -> FORMULA f) -> Named (FORMULA f) -> Named (FORMULA f)
forall s t a. (s -> t) -> SenAttr s a -> SenAttr t a
mapNamed ((FORMULA f -> FORMULA f)
 -> Named (FORMULA f) -> Named (FORMULA f))
-> (FORMULA f -> FORMULA f)
-> Named (FORMULA f)
-> Named (FORMULA f)
forall a b. (a -> b) -> a -> b
$ MapSen f e () -> Morphism f e () -> FORMULA f -> FORMULA f
forall f e m.
MapSen f e m -> Morphism f e m -> FORMULA f -> FORMULA f
MapSen.mapMorphForm ((f -> f) -> MapSen f e ()
forall a b. a -> b -> a
const f -> f
forall a. a -> a
id) Morphism f e ()
mor) [Named (FORMULA f)]
sens
  (s :: Sign
s, l :: [Named Axiom]
l) <- Sign f e -> Result (Sign, [Named Axiom])
forall f e. Sign f e -> Result (Sign, [Named Axiom])
mapSign Sign f e
tar
  [[Named Axiom]]
ll <- (Named (FORMULA f) -> Result [Named Axiom])
-> [Named (FORMULA f)] -> Result [[Named Axiom]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\ ns :: Named (FORMULA f)
ns -> case Named (FORMULA f) -> FORMULA f
forall s a. SenAttr s a -> s
sentence Named (FORMULA f)
ns of
    Sort_gen_ax cs :: [Constraint]
cs b :: Bool
b -> [Named Axiom] -> Result [Named Axiom]
forall (m :: * -> *) a. Monad m => a -> m a
return ([Named Axiom] -> Result [Named Axiom])
-> [Named Axiom] -> Result [Named Axiom]
forall a b. (a -> b) -> a -> b
$ [Constraint] -> Bool -> [Named Axiom]
mapSortGenAx [Constraint]
cs Bool
b
    _ -> (String -> Range -> Result [Named Axiom])
-> Range -> String -> Result [Named Axiom]
forall a b c. (a -> b -> c) -> b -> a -> c
flip ([Named Axiom] -> String -> Range -> Result [Named Axiom]
forall a. a -> String -> Range -> Result a
hint []) Range
nullRange
         (String -> Result [Named Axiom])
-> (Named (FORMULA f) -> String)
-> Named (FORMULA f)
-> Result [Named Axiom]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ("not translated\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++) ShowS
-> (Named (FORMULA f) -> String) -> Named (FORMULA f) -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> String
forall a. Show a => a -> String
show (Doc -> String)
-> (Named (FORMULA f) -> Doc) -> Named (FORMULA f) -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Named (FORMULA f) -> Doc
forall f. FormExtension f => Named (FORMULA f) -> Doc
printTheoryFormula
         (Named (FORMULA f) -> Result [Named Axiom])
-> Named (FORMULA f) -> Result [Named Axiom]
forall a b. (a -> b) -> a -> b
$ (FORMULA f -> FORMULA f) -> Named (FORMULA f) -> Named (FORMULA f)
forall s t a. (s -> t) -> SenAttr s a -> SenAttr t a
mapNamed (Min f e
-> (Sign f e -> f -> f) -> Sign f e -> FORMULA f -> FORMULA f
forall f e.
(FormExtension f, TermExtension f) =>
Min f e
-> (Sign f e -> f -> f) -> Sign f e -> FORMULA f -> FORMULA f
simplifySen ((f -> Result f) -> Min f e
forall a b. a -> b -> a
const f -> Result f
forall (m :: * -> *) a. Monad m => a -> m a
return) ((f -> f) -> Sign f e -> f -> f
forall a b. a -> b -> a
const f -> f
forall a. a -> a
id) Sign f e
tar) Named (FORMULA f)
ns
             ) [Named (FORMULA f)]
nss
  (Sign, [Named Axiom]) -> Result (Sign, [Named Axiom])
forall (m :: * -> *) a. Monad m => a -> m a
return (Sign
s, [Named Axiom]
l [Named Axiom] -> [Named Axiom] -> [Named Axiom]
forall a. [a] -> [a] -> [a]
++ [[Named Axiom]] -> [Named Axiom]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[Named Axiom]]
ll)

mapSortGenAx :: [Constraint] -> Bool -> [Named Axiom]
mapSortGenAx :: [Constraint] -> Bool -> [Named Axiom]
mapSortGenAx cs :: [Constraint]
cs b :: Bool
b = ((Id, [OP_SYMB]) -> Named Axiom)
-> [(Id, [OP_SYMB])] -> [Named Axiom]
forall a b. (a -> b) -> [a] -> [b]
map (\ (s :: Id
s, as :: [OP_SYMB]
as) ->
  let is :: [ClassExpression]
is = (OP_SYMB -> ClassExpression) -> [OP_SYMB] -> [ClassExpression]
forall a b. (a -> b) -> [a] -> [b]
map (\ (Qual_op_name n :: Id
n ty :: OP_TYPE
ty _) -> case OP_TYPE -> [Id]
args_OP_TYPE OP_TYPE
ty of
                [] -> [Class] -> ClassExpression
ObjectOneOf [Id -> Class
idToIRI Id
n]
                [_] -> QuantifierType
-> ObjectPropertyExpression -> ClassExpression -> ClassExpression
ObjectValuesFrom QuantifierType
SomeValuesFrom (Id -> Int -> ObjectPropertyExpression
toO Id
n (-1)) (ClassExpression -> ClassExpression)
-> ClassExpression -> ClassExpression
forall a b. (a -> b) -> a -> b
$ Id -> ClassExpression
toC Id
s
                _ -> Id -> ClassExpression
toC Id
n) [OP_SYMB]
as
  in String -> Axiom -> Named Axiom
forall a s. a -> s -> SenAttr s a
makeNamed ("generated " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Id -> String
forall a. Show a => a -> String
show Id
s) (Axiom -> Named Axiom) -> Axiom -> Named Axiom
forall a b. (a -> b) -> a -> b
$ ClassAxiom -> Axiom
ClassAxiom (ClassAxiom -> Axiom) -> ClassAxiom -> Axiom
forall a b. (a -> b) -> a -> b
$
    if Bool
b Bool -> Bool -> Bool
&& Bool -> Bool
not ([ClassExpression] -> Bool
forall a. [a] -> Bool
isSingle [ClassExpression]
is) then AxiomAnnotations -> Class -> [ClassExpression] -> ClassAxiom
DisjointUnion [] (Id -> Class
idToIRI Id
s) [ClassExpression]
is
    else AxiomAnnotations -> [ClassExpression] -> ClassAxiom
EquivalentClasses [] ([ClassExpression] -> ClassAxiom)
-> [ClassExpression] -> ClassAxiom
forall a b. (a -> b) -> a -> b
$ [Id -> ClassExpression
toC Id
s, case [ClassExpression]
is of
        [i :: ClassExpression
i] -> ClassExpression
i
        _ -> JunctionType -> [ClassExpression] -> ClassExpression
ObjectJunction JunctionType
UnionOf [ClassExpression]
is])
  ([(Id, [OP_SYMB])] -> [Named Axiom])
-> [(Id, [OP_SYMB])] -> [Named Axiom]
forall a b. (a -> b) -> a -> b
$ [Constraint] -> [(Id, [OP_SYMB])]
recoverSortGen [Constraint]
cs