Merge pull request #1672 from spechub/owl-datatypes-in-casl

Owl datatypes in casl

CASL_DL/PredefinedCASLAxioms.hs

@@ -13,6 +13,8 @@ Portability :  portable
 module CASL_DL.PredefinedCASLAxioms
   ( predefSign
   , predefinedSign
+  , predefSign2
+  , datatypeSigns
   , thing
   , nothing
   , conceptPred
@@ -52,6 +54,8 @@ import Common.GlobalAnnotations
 import qualified Common.Lib.Rel as Rel
 import qualified Common.Lib.MapSet as MapSet
 
+import qualified Data.Map as Map
+
 import Data.Char
 
 hetsPrefix :: String
@@ -231,6 +235,53 @@ noThing = Qual_pred_name nothing classPredType n
 intTypes :: [PredType]
 intTypes = map (\ t -> PredType [t]) [integer, nonNegInt]
 
+predefinedSign2 :: e -> Sign f e
+predefinedSign2 e = (emptySign e) {
+  sortRel = Rel.insertKey thing $ Rel.insertKey dataS Rel.empty
+  }
+
+predefSign2 :: CASLSign
+predefSign2 = predefinedSign2 ()
+
+-- | instead of one big signature, several small ones
+
+charSign :: CASLSign
+charSign = (emptySign ())
+                 { sortRel = Rel.insertKey (stringToId "Char") Rel.empty
+                 , opMap = MapSet.fromList
+                        $  map (\ c -> (charToId c, [charT]))
+                          [chr 0 .. chr 127]
+                 }
+
+integerSign :: CASLSign
+integerSign  = (emptySign ())
+                 { sortRel =
+                      Rel.transClosure $ Rel.fromList
+                       [(negIntS, nonPosInt),
+                        (nonNegInt, integer),
+                        (nonPosInt, integer),
+                        (posInt, nonNegInt),
+                        (integer, dataS)]
+                 , predMap =
+                     MapSet.fromList
+                      $ 
+                      map ( \ o -> (stringToId o, intTypes))
+                         ["even", "odd"]
+                 , opMap = MapSet.fromList
+                        $ map (\ i -> (stringToId $ show i, [natT]))
+                          [0 .. 9 :: Int]
+                        ++
+                        [ 
+                         (atAt, [atAtTy])
+                        ]
+                 , globAnnos = emptyGlobalAnnos
+                     { literal_annos = emptyLiteralAnnos
+                       { number_lit = Just atAt
+                        }}
+                 }
+
+
+
 predefinedSign :: e -> Sign f e
 predefinedSign e = (emptySign e)
                  { sortRel = Rel.insertKey (stringToId "Char")
@@ -273,6 +324,67 @@ predefinedSign e = (emptySign e)
                        , string_lit = Just (emptyString, cons) }}
                  }
 
+floatSign :: CASLSign
+floatSign = integerSign
+                 { sortRel = Rel.union (sortRel integerSign) 
+                      $ Rel.transClosure $ Rel.fromList
+                       [
+                        (integer, float),
+                        (float, dataS)
+                        ]
+
+                 , opMap = MapSet.union (opMap integerSign) $ MapSet.fromList
+                        $ 
+                        [
+                          (unMinus, [minusTy, minusFloat])
+                        , (dec, [decTy])
+                        , (eId, [expTy])
+                        ]
+                 , globAnnos = (globAnnos integerSign)
+                     { literal_annos = (literal_annos $ globAnnos integerSign)
+                       {  float_lit = Just (dec, eId)
+                        }}
+                 }
+
+boolSign :: CASLSign
+boolSign = (emptySign ())
+                 { sortRel =  Rel.transClosure $ Rel.fromList
+                       [(boolS, dataS)]
+                 , opMap = MapSet.fromList
+                        $ 
+                        [ (trueS, [boolT])
+                        , (falseS, [boolT])
+                        ]
+                 }
+
+stringSignAux :: CASLSign
+stringSignAux = (emptySign ())
+                 { sortRel = 
+                      Rel.transClosure $ Rel.fromList
+                       [ (stringS, dataS) ]
+                 , opMap = MapSet.fromList
+                        $ 
+                        [
+                         (emptyString, [emptyStringTy])
+                         , (cons, [consTy])
+                        ]
+                 , globAnnos = emptyGlobalAnnos
+                     { literal_annos = emptyLiteralAnnos
+                       { 
+                       string_lit = Just (emptyString, cons) }}
+                 }
+
+stringSign :: CASLSign
+stringSign = uniteCASLSign stringSignAux charSign
+
+datatypeSigns :: Map.Map SORT CASLSign
+datatypeSigns = Map.fromList
+   [ (charS, charSign)
+   , (integer, integerSign)
+   , (float, floatSign)
+   , (boolS, boolSign)
+   , (stringS, stringSign)]
+
 predefSign :: CASLSign
 predefSign = predefinedSign ()
 
@@ -287,7 +399,7 @@ predefinedAxioms = let
 
 mkNNameAux :: Int -> String
 mkNNameAux k = genNamePrefix ++ "x" ++ show k
- 
+
 -- | Build a name
 mkNName :: Int -> Token
 mkNName i = mkSimpleId $ hetsPrefix ++ mkNNameAux i

Logic/Logic.hs

@@ -395,14 +395,14 @@ symset_of :: forall lid sentence sign morphism symbol .
 symset_of lid sig = Set.unions $ sym_of lid sig
 
 -- | check that all sentence names in a theory do not appear as symbol names
-checkSenNames :: forall lid sentence sign morphism symbol . 
+checkSenNames :: forall lid sentence sign morphism symbol .
                  Sentences lid sentence sign morphism symbol =>
                  lid -> sign -> [Named sentence] -> Set.Set String
-checkSenNames lid aSig nsens = 
+checkSenNames lid aSig nsens =
  let senNames = map senAttr nsens
      symNames = map (show . (sym_name lid)) $ Set.toList $
                 symset_of lid aSig
- in Set.intersection (Set.fromList symNames) $ Set.fromList senNames 
+ in Set.intersection (Set.fromList symNames) $ Set.fromList senNames
 
 -- | dependency ordered list of symbols for a signature
 symlist_of :: forall lid sentence sign morphism symbol .
@@ -627,7 +627,7 @@ class ( Syntax lid basic_spec symbol symb_items symb_map_items
          equiv2cospan :: lid -> sign -> sign -> [symb_items] -> [symb_items]
            -> Result (sign, sign, sign, EndoMap symbol, EndoMap symbol)
          equiv2cospan _ _ _ _ _ = error "equiv2cospan nyi"
-         -- | extract the module 
+         -- | extract the module
          extract_module :: lid -> [IRI] -> (sign, [Named sentence])
                         -> Result (sign, [Named sentence])
          extract_module _ _ = return
@@ -850,6 +850,17 @@ class (StaticAnalysis lid
          -- no logic should throw an error here
          addOmdocToTheory _ _ t _ = return t
 
+
+-- | sublogic of a theory
+sublogicOfTheo :: (Logic lid sublogics
+        basic_spec sentence symb_items symb_map_items
+        sign morphism symbol raw_symbol proof_tree) =>
+    lid -> (sign, [sentence]) -> sublogics
+sublogicOfTheo _ (sig, axs) =
+  foldl lub (minSublogic sig) $
+  map minSublogic axs
+
+
 {- The class of logics which can be used as logical frameworks, in which object
    logics can be specified by the user. Currently the only logics implementing
    this class are LF, Maude, and Isabelle, with the latter two only having

OWL2/OWL22CASL.hs

@@ -39,6 +39,7 @@ import OWL2.ManchesterPrint ()
 import OWL2.Morphism
 import OWL2.Symbols
 import qualified OWL2.Sign as OS
+import qualified OWL2.Sublogic as SL
 -- CASL_DL = codomain
 import CASL.Logic_CASL
 import CASL.AS_Basic_CASL
@@ -122,13 +123,13 @@ uriToCaslId urI = let
  in
   if ((isDatatypeKey urI) && (isThing urI))  then
         getId $ localPart urI
-   else 
+   else {-
     let
       ePart = expandedIRI urI
     in
       if ePart /= "" then
         getId $ expandedIRI urI
-      else 
+      else -}
         getId $ localPart urI
 
 tokDecl :: Token -> VAR_DECL
@@ -252,27 +253,35 @@ mapSign sig =
             [ tMp conceptPred cPreds
             , tMp objectPropPred oPreds
             , tMp dataPropPred dPreds ]
-     in return $ uniteCASLSign predefSign (emptySign ())
+     in return $  uniteCASLSign predefSign2
+         (emptySign ())
              { predMap = aPreds
              , opMap = tMp indiConst . cvrt $ OS.individuals sig
              }
 
-loadDataInformation :: ProfSub -> Sign f ()
-loadDataInformation _ = let dts = Set.fromList $ map stringToId datatypeKeys
-    in  (emptySign ()) { sortRel = Rel.fromKeysSet dts }
+loadDataInformation :: ProfSub -> CASLSign
+loadDataInformation sl = let
+  dts = Set.map uriToCaslId $ SL.datatype $ sublogic sl
+  eSig x = (emptySign ()) { sortRel =
+       Rel.fromList  [(x, dataS)]}
+  sigs = Set.toList $
+         Set.map (\x -> Map.findWithDefault (eSig x) x datatypeSigns) dts
+ in  foldl uniteCASLSign (emptySign ()) sigs
 
 mapTheory :: (OS.Sign, [Named Axiom]) -> Result (CASLSign, [Named CASLFORMULA])
-mapTheory (owlSig, owlSens) = let sl = topS in do
+mapTheory (owlSig, owlSens) = let
+  sl = sublogicOfTheo OWL2 (owlSig, map sentence owlSens)
+ in do
     cSig <- mapSign owlSig
     let pSig = loadDataInformation sl
-        dTypes = (emptySign ()) {sortRel = Rel.transClosure . Rel.fromSet
+        {- dTypes = (emptySign ()) {sortRel = Rel.transClosure . Rel.fromSet
                     . Set.map (\ d -> (uriToCaslId d, dataS))
-                    . Set.union predefIRIs $ OS.datatypes owlSig}
+                    . Set.union predefIRIs $ OS.datatypes owlSig} -}
     (cSens, nSig) <- foldM (\ (x, y) z -> do
             (sen, sig) <- mapSentence y z
             return (sen ++ x, uniteCASLSign sig y)) ([], cSig) owlSens
-    return (foldl1 uniteCASLSign [nSig, pSig, dTypes],
-                predefinedAxioms ++ (reverse cSens))
+    return (foldl1 uniteCASLSign [nSig, pSig],  -- , dTypes],
+            predefinedAxioms ++ (reverse cSens))
 
 -- | mapping of OWL to CASL_DL formulae
 mapSentence :: CASLSign -> Named Axiom -> Result ([Named CASLFORMULA], CASLSign)
@@ -640,6 +649,17 @@ mkEDPairs s il mr pairs = do
                 _ -> error "expected EDRelation") pairs
     return (ls, s)
 
+mkEDPairs' :: CASLSign -> [Int] -> Maybe O.Relation -> [(FORMULA f, FORMULA f)]
+    -> Result ([FORMULA f], CASLSign)
+mkEDPairs' s [i1, i2] mr pairs = do
+    let ls = map (\ (x, y) -> mkVDecl [i1] $ mkVDataDecl [i2]
+            $ case fromMaybe (error "expected EDRelation") mr of
+                EDRelation Equivalent -> mkEqv x y
+                EDRelation Disjoint -> mkNC [x, y]
+                _ -> error "expected EDRelation") pairs
+    return (ls, s)
+mkEDPairs' _ _ _ _ = error "wrong call of mkEDPairs'"
+
 -- | Mapping of ListFrameBit
 mapListFrameBit :: CASLSign -> Extended -> Maybe O.Relation -> ListFrameBit
        -> Result ([CASLFORMULA], CASLSign)
@@ -716,16 +736,16 @@ mapListFrameBit cSig ex rel lfb =
       Just r -> case ex of
         Misc _ -> do
             pairs <- mapComDataPropsList cSig Nothing dl 1 2
-            mkEDPairs cSig [1, 2] rel pairs
+            mkEDPairs' cSig [1, 2] rel pairs
         SimpleEntity (Entity _ DataProperty iri) -> case r of
             SubPropertyOf -> do
                 os1 <- mapM (\ o1 -> mapDataProp cSig o1 1 2) dl
-                o2 <- mapDataProp cSig iri 2 1
+                o2 <- mapDataProp cSig iri 1 2 -- was 2 1
                 return (map (mkForall [thingDecl 1, dataDecl 2]
                     . mkImpl o2) os1, cSig)
             EDRelation _ -> do
                 pairs <- mapComDataPropsList cSig (Just iri) dl 1 2
-                mkEDPairs cSig [1, 2] rel pairs
+                mkEDPairs' cSig [1, 2] rel pairs
             _ -> return ([], cSig)
         _ -> err
     IndividualSameOrDifferent al -> case rel of