{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances #-}
{-# OPTIONS -w #-}
{- |
Module      :  ./RDF/Logic_RDF.hs
Description :  instance of the class Logic for RDF
Copyright   :  (c) Felix Mance
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  f.mance@jacobs-university.de
Stability   :  provisional
Portability :  non-portable

Here is the place where the class Logic is instantiated for RDF
-}

module RDF.Logic_RDF where

import ATC.ProofTree ()

import Common.AS_Annotation
import Common.Consistency
import Common.DefaultMorphism
import Common.Doc
import Common.DocUtils
import Common.ProofTree
import Common.ProverTools

import qualified Data.Map as Map
import Data.Monoid

import Logic.Logic

import RDF.AS
--import RDF.ATC_RDF ()
import RDF.Parse
import RDF.Symbols
import RDF.Print
import RDF.Sign
import RDF.Morphism
import RDF.Sublogic
import RDF.StaticAnalysis
import ATerm.Conversion
import RDF.ATC_RDF ()

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

instance Language RDF where
  language_name :: RDF -> String
language_name _ = "RDF"
  description :: RDF -> String
description _ =
    "RDF -- Resource Description Framework http://www.w3.org/RDF/"

instance Category Sign RDFMorphism where
    {- }ide sig = inclRDFMorphism sig sig
    dom = osource
    cod = otarget
    legal_mor = legalMor
    isInclusion = isRDFInclusion
    composeMorphisms = composeMor
-}

instance Semigroup TurtleDocument where
    (TurtleDocument i :: IRI
i p1 :: RDFPrefixMap
p1 l1 :: [Statement]
l1) <> :: TurtleDocument -> TurtleDocument -> TurtleDocument
<> (TurtleDocument _ p2 :: RDFPrefixMap
p2 l2 :: [Statement]
l2) =
      IRI -> RDFPrefixMap -> [Statement] -> TurtleDocument
TurtleDocument IRI
i (RDFPrefixMap -> RDFPrefixMap -> RDFPrefixMap
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union RDFPrefixMap
p1 RDFPrefixMap
p2) ([Statement] -> TurtleDocument) -> [Statement] -> TurtleDocument
forall a b. (a -> b) -> a -> b
$ [Statement]
l1 [Statement] -> [Statement] -> [Statement]
forall a. [a] -> [a] -> [a]
++ [Statement]
l2
instance Monoid TurtleDocument where
    mempty :: TurtleDocument
mempty = TurtleDocument
emptyTurtleDocument

instance Syntax RDF TurtleDocument RDFEntity SymbItems SymbMapItems where
    parse_basic_spec :: RDF -> Maybe (RDFPrefixMap -> AParser st TurtleDocument)
parse_basic_spec RDF = (RDFPrefixMap -> AParser st TurtleDocument)
-> Maybe (RDFPrefixMap -> AParser st TurtleDocument)
forall a. a -> Maybe a
Just RDFPrefixMap -> AParser st TurtleDocument
forall st. RDFPrefixMap -> CharParser st TurtleDocument
basicSpec
    parse_symb_items :: RDF -> Maybe (RDFPrefixMap -> AParser st SymbItems)
parse_symb_items RDF = (RDFPrefixMap -> AParser st SymbItems)
-> Maybe (RDFPrefixMap -> AParser st SymbItems)
forall a. a -> Maybe a
Just ((RDFPrefixMap -> AParser st SymbItems)
 -> Maybe (RDFPrefixMap -> AParser st SymbItems))
-> (AParser st SymbItems -> RDFPrefixMap -> AParser st SymbItems)
-> AParser st SymbItems
-> Maybe (RDFPrefixMap -> AParser st SymbItems)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AParser st SymbItems -> RDFPrefixMap -> AParser st SymbItems
forall a b. a -> b -> a
const (AParser st SymbItems
 -> Maybe (RDFPrefixMap -> AParser st SymbItems))
-> AParser st SymbItems
-> Maybe (RDFPrefixMap -> AParser st SymbItems)
forall a b. (a -> b) -> a -> b
$ AParser st SymbItems
forall st. GenParser Char st SymbItems
rdfSymbItems
    parse_symb_map_items :: RDF -> Maybe (RDFPrefixMap -> AParser st SymbMapItems)
parse_symb_map_items RDF = (RDFPrefixMap -> AParser st SymbMapItems)
-> Maybe (RDFPrefixMap -> AParser st SymbMapItems)
forall a. a -> Maybe a
Just ((RDFPrefixMap -> AParser st SymbMapItems)
 -> Maybe (RDFPrefixMap -> AParser st SymbMapItems))
-> (AParser st SymbMapItems
    -> RDFPrefixMap -> AParser st SymbMapItems)
-> AParser st SymbMapItems
-> Maybe (RDFPrefixMap -> AParser st SymbMapItems)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AParser st SymbMapItems -> RDFPrefixMap -> AParser st SymbMapItems
forall a b. a -> b -> a
const (AParser st SymbMapItems
 -> Maybe (RDFPrefixMap -> AParser st SymbMapItems))
-> AParser st SymbMapItems
-> Maybe (RDFPrefixMap -> AParser st SymbMapItems)
forall a b. (a -> b) -> a -> b
$ AParser st SymbMapItems
forall st. GenParser Char st SymbMapItems
rdfSymbMapItems

instance Sentences RDF Axiom Sign RDFMorphism RDFEntity where
    -- map_sen RDF = mapSen
    print_named :: RDF -> Named Axiom -> Doc
print_named RDF namedSen :: Named Axiom
namedSen = Axiom -> Doc
forall a. Pretty a => a -> Doc
pretty (Axiom -> Doc) -> Axiom -> Doc
forall a b. (a -> b) -> a -> b
$ Named Axiom -> Axiom
forall s a. SenAttr s a -> s
sentence Named Axiom
namedSen
    {- sym_of RDF = singletonList . symOf
    symmap_of RDF = symMapOf -}

instance StaticAnalysis RDF TurtleDocument Axiom
               SymbItems SymbMapItems
               Sign
               RDFMorphism
               RDFEntity RawSymb where
      basic_analysis :: RDF
-> Maybe
     ((TurtleDocument, Sign, GlobalAnnos)
      -> Result (TurtleDocument, ExtSign Sign RDFEntity, [Named Axiom]))
basic_analysis RDF = ((TurtleDocument, Sign, GlobalAnnos)
 -> Result (TurtleDocument, ExtSign Sign RDFEntity, [Named Axiom]))
-> Maybe
     ((TurtleDocument, Sign, GlobalAnnos)
      -> Result (TurtleDocument, ExtSign Sign RDFEntity, [Named Axiom]))
forall a. a -> Maybe a
Just (TurtleDocument, Sign, GlobalAnnos)
-> Result (TurtleDocument, ExtSign Sign RDFEntity, [Named Axiom])
basicRDFAnalysis
      {- stat_symb_items RDF _ = return . statSymbItems
      stat_symb_map_items RDF _ _ = statSymbMapItems -}
      empty_signature :: RDF -> Sign
empty_signature RDF = Sign
emptySign
      signature_union :: RDF -> Sign -> Sign -> Result Sign
signature_union RDF = Sign -> Sign -> Result Sign
uniteSign
      signatureDiff :: RDF -> Sign -> Sign -> Result Sign
signatureDiff RDF s :: Sign
s = Sign -> Result Sign
forall (m :: * -> *) a. Monad m => a -> m a
return (Sign -> Result Sign) -> (Sign -> Sign) -> Sign -> Result Sign
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sign -> Sign -> Sign
diffSig Sign
s
      final_union :: RDF -> Sign -> Sign -> Result Sign
final_union RDF = RDF -> Sign -> Sign -> Result Sign
forall lid basic_spec sentence symb_items symb_map_items sign
       morphism symbol raw_symbol.
StaticAnalysis
  lid
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol =>
lid -> sign -> sign -> Result sign
signature_union RDF
RDF
      is_subsig :: RDF -> Sign -> Sign -> Bool
is_subsig RDF = Sign -> Sign -> Bool
isSubSign
      {- subsig_inclusion RDF s = return . inclRDFMorphism s
      matches RDF = matchesSym -}
      symbol_to_raw :: RDF -> RDFEntity -> RawSymb
symbol_to_raw RDF = RDFEntity -> RawSymb
ASymbol
      {- induced_from_morphism RDF = inducedFromMor
      cogenerated_sign RDF = cogeneratedSign
      generated_sign RDF = generatedSign -}

instance Logic RDF RDFSub TurtleDocument Axiom SymbItems SymbMapItems
               Sign
               RDFMorphism RDFEntity RawSymb ProofTree where
         empty_proof_tree :: RDF -> ProofTree
empty_proof_tree RDF = ProofTree
emptyProofTree
         stability :: RDF -> Stability
stability RDF = Stability
Experimental

{-
instance SemiLatticeWithTop ProfSub where
    join = maxS
    top = topS

instance SublogicName ProfSub where
    sublogicName = nameS

instance MinSublogic ProfSub Axiom where
    minSublogic = psAxiom

instance MinSublogic ProfSub OWLMorphism where
    minSublogic = sMorph

instance ProjectSublogic ProfSub OWLMorphism where
    projectSublogic = prMorph

instance MinSublogic ProfSub Sign where
    minSublogic = sSig

instance ProjectSublogic ProfSub Sign where
    projectSublogic = prSign

instance MinSublogic ProfSub SymbItems where
    minSublogic = const topS

instance MinSublogic ProfSub SymbMapItems where
    minSublogic = const topS

instance MinSublogic ProfSub Entity where
    minSublogic = const topS

instance MinSublogic ProfSub OntologyDocument where
    minSublogic = profilesAndSublogic

instance ProjectSublogicM ProfSub SymbItems where
    projectSublogicM = const Just

instance ProjectSublogicM ProfSub SymbMapItems where
    projectSublogicM = const Just

instance ProjectSublogicM ProfSub Entity where
    projectSublogicM = const Just

instance ProjectSublogic ProfSub OntologyDocument where
    projectSublogic = prOntDoc
-}