{-# LANGUAGE CPP, MultiParamTypeClasses #-}

{- |
Module      :  ./NeSyPatterns/Logic_NeSyPatterns.hs
Description :  Instance of class Logic for neural-symbolic patterns
Copyright   :  (c) Till Mossakowski, Uni Magdeburg 2022
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  till.mossakowski@ovgu.de
Stability   :  experimental
Portability :  non-portable (imports Logic.Logic)

Instance of class Logic for neural-symbolic patterns
-}

module NeSyPatterns.Logic_NeSyPatterns where

import Logic.Logic

import OWL2.Logic_OWL2

import NeSyPatterns.Analysis
import NeSyPatterns.AS
import NeSyPatterns.Morphism
import NeSyPatterns.Sign
import NeSyPatterns.Symbol as Symbol
import NeSyPatterns.Parse
#ifdef UNI_PACKAGE
import NeSyPatterns.Taxonomy (nesy2Tax)
#endif

import Common.ProofTree
import ATC.ProofTree ()

import NeSyPatterns.ATC_NeSyPatterns ()

import qualified Data.Map as Map

-- | Lid for propositional logic
data NeSyPatterns = NeSyPatterns deriving Int -> NeSyPatterns -> ShowS
[NeSyPatterns] -> ShowS
NeSyPatterns -> String
(Int -> NeSyPatterns -> ShowS)
-> (NeSyPatterns -> String)
-> ([NeSyPatterns] -> ShowS)
-> Show NeSyPatterns
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [NeSyPatterns] -> ShowS
$cshowList :: [NeSyPatterns] -> ShowS
show :: NeSyPatterns -> String
$cshow :: NeSyPatterns -> String
showsPrec :: Int -> NeSyPatterns -> ShowS
$cshowsPrec :: Int -> NeSyPatterns -> ShowS
Show

instance Language NeSyPatterns where
    description :: NeSyPatterns -> String
description _ = "NeSyPatterns Logic\n"
        String -> ShowS
forall a. [a] -> [a] -> [a]
++ "for more information please refer to\n"
        String -> ShowS
forall a. [a] -> [a] -> [a]
++ "http://en.wikipedia.org/wiki/NeSyPatterns_logic"

-- | Instance of Category for propositional logic
instance Category Sign Morphism where
    -- Identity morhpism
    ide :: Sign -> Morphism
ide = Sign -> Morphism
idMor
    -- Returns the domain of a morphism
    dom :: Morphism -> Sign
dom = Morphism -> Sign
source
    -- Returns the codomain of a morphism
    cod :: Morphism -> Sign
cod = Morphism -> Sign
target
    -- check if morphism is inclusion
    isInclusion :: Morphism -> Bool
isInclusion = Map ResolvedNode ResolvedNode -> Bool
forall k a. Map k a -> Bool
Map.null (Map ResolvedNode ResolvedNode -> Bool)
-> (Morphism -> Map ResolvedNode ResolvedNode) -> Morphism -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Morphism -> Map ResolvedNode ResolvedNode
nodeMap
    -- tests if the morphism is ok
    legal_mor :: Morphism -> Result ()
legal_mor = Morphism -> Result ()
isLegalMorphism
    -- composition of morphisms
    composeMorphisms :: Morphism -> Morphism -> Result Morphism
composeMorphisms = Morphism -> Morphism -> Result Morphism
composeMor

-- | Instance of Sentences for propositional logic
instance Sentences NeSyPatterns ()
    Sign Morphism Symbol where
    negation :: NeSyPatterns -> () -> Maybe ()
negation NeSyPatterns _ = () -> Maybe ()
forall a. a -> Maybe a
Just ()
    -- returns the set of symbols
    sym_of :: NeSyPatterns -> Sign -> [Set Symbol]
sym_of NeSyPatterns = Set Symbol -> [Set Symbol]
forall a. a -> [a]
singletonList (Set Symbol -> [Set Symbol])
-> (Sign -> Set Symbol) -> Sign -> [Set Symbol]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sign -> Set Symbol
symOf
    -- returns the symbol map
    symmap_of :: NeSyPatterns -> Morphism -> EndoMap Symbol
symmap_of NeSyPatterns = Morphism -> EndoMap Symbol
getSymbolMap
    -- returns the name of a symbol
    sym_name :: NeSyPatterns -> Symbol -> Id
sym_name NeSyPatterns = Symbol -> Id
getSymbolName
    symKind :: NeSyPatterns -> Symbol -> String
symKind NeSyPatterns _ = "prop"
    -- translation of sentences along signature morphism
    map_sen :: NeSyPatterns -> Morphism -> () -> Result ()
map_sen NeSyPatterns _ = Result () -> () -> Result ()
forall (m :: * -> *) a. Monad m => a -> m a
return (Result () -> () -> Result ()) -> Result () -> () -> Result ()
forall a b. (a -> b) -> a -> b
$ () -> Result ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    -- there is nothing to leave out
    simplify_sen :: NeSyPatterns -> Sign -> () -> ()
simplify_sen NeSyPatterns _ _ = ()


instance Semigroup BASIC_SPEC where
    (Basic_spec paths1 :: [Annoted BASIC_ITEM]
paths1) <> :: BASIC_SPEC -> BASIC_SPEC -> BASIC_SPEC
<> (Basic_spec paths2 :: [Annoted BASIC_ITEM]
paths2) = [Annoted BASIC_ITEM] -> BASIC_SPEC
Basic_spec ([Annoted BASIC_ITEM]
paths1 [Annoted BASIC_ITEM]
-> [Annoted BASIC_ITEM] -> [Annoted BASIC_ITEM]
forall a. [a] -> [a] -> [a]
++ [Annoted BASIC_ITEM]
paths2)

instance Monoid BASIC_SPEC where
    mempty :: BASIC_SPEC
mempty = [Annoted BASIC_ITEM] -> BASIC_SPEC
Basic_spec []
    mappend :: BASIC_SPEC -> BASIC_SPEC -> BASIC_SPEC
mappend (Basic_spec l1 :: [Annoted BASIC_ITEM]
l1) (Basic_spec l2 :: [Annoted BASIC_ITEM]
l2) = [Annoted BASIC_ITEM] -> BASIC_SPEC
Basic_spec ([Annoted BASIC_ITEM] -> BASIC_SPEC)
-> [Annoted BASIC_ITEM] -> BASIC_SPEC
forall a b. (a -> b) -> a -> b
$ [Annoted BASIC_ITEM]
l1 [Annoted BASIC_ITEM]
-> [Annoted BASIC_ITEM] -> [Annoted BASIC_ITEM]
forall a. [a] -> [a] -> [a]
++ [Annoted BASIC_ITEM]
l2

-- - | Syntax of NeSyPatterns logic
instance Syntax NeSyPatterns BASIC_SPEC
    Symbol SYMB_ITEMS SYMB_MAP_ITEMS where
         parsersAndPrinters :: NeSyPatterns
-> Map
     String (PrefixMap -> AParser st BASIC_SPEC, BASIC_SPEC -> Doc)
parsersAndPrinters NeSyPatterns =
           String
-> (PrefixMap -> AParser st BASIC_SPEC, BASIC_SPEC -> Doc)
-> Map
     String (PrefixMap -> AParser st BASIC_SPEC, BASIC_SPEC -> Doc)
-> Map
     String (PrefixMap -> AParser st BASIC_SPEC, BASIC_SPEC -> Doc)
forall b. String -> b -> Map String b -> Map String b
addSyntax "Hets" (PrefixMap -> AParser st BASIC_SPEC
forall st. PrefixMap -> AParser st BASIC_SPEC
basicSpec, BASIC_SPEC -> Doc
forall a. Pretty a => a -> Doc
pretty)
           (Map String (PrefixMap -> AParser st BASIC_SPEC, BASIC_SPEC -> Doc)
 -> Map
      String (PrefixMap -> AParser st BASIC_SPEC, BASIC_SPEC -> Doc))
-> Map
     String (PrefixMap -> AParser st BASIC_SPEC, BASIC_SPEC -> Doc)
-> Map
     String (PrefixMap -> AParser st BASIC_SPEC, BASIC_SPEC -> Doc)
forall a b. (a -> b) -> a -> b
$ (PrefixMap -> AParser st BASIC_SPEC, BASIC_SPEC -> Doc)
-> Map
     String (PrefixMap -> AParser st BASIC_SPEC, BASIC_SPEC -> Doc)
forall b. b -> Map String b
makeDefault (PrefixMap -> AParser st BASIC_SPEC
forall st. PrefixMap -> AParser st BASIC_SPEC
basicSpec, BASIC_SPEC -> Doc
forall a. Pretty a => a -> Doc
pretty)
         parse_symb_items :: NeSyPatterns -> Maybe (PrefixMap -> AParser st SYMB_ITEMS)
parse_symb_items NeSyPatterns = (PrefixMap -> AParser st SYMB_ITEMS)
-> Maybe (PrefixMap -> AParser st SYMB_ITEMS)
forall a. a -> Maybe a
Just PrefixMap -> AParser st SYMB_ITEMS
forall st. PrefixMap -> AParser st SYMB_ITEMS
symbItems
         parse_symb_map_items :: NeSyPatterns -> Maybe (PrefixMap -> AParser st SYMB_MAP_ITEMS)
parse_symb_map_items NeSyPatterns = (PrefixMap -> AParser st SYMB_MAP_ITEMS)
-> Maybe (PrefixMap -> AParser st SYMB_MAP_ITEMS)
forall a. a -> Maybe a
Just PrefixMap -> AParser st SYMB_MAP_ITEMS
forall st. PrefixMap -> AParser st SYMB_MAP_ITEMS
symbMapItems

-- | Instance of Logic for propositional logc
instance Logic NeSyPatterns
    ()                    -- Sublogics
    BASIC_SPEC                -- basic_spec
    ()                   -- sentence
    SYMB_ITEMS                -- symb_items
    SYMB_MAP_ITEMS            -- symb_map_items
    Sign                          -- sign
    Morphism                  -- morphism
    Symbol                      -- symbol
    Symbol                      -- raw_symbol
    ProofTree                      -- proof_tree
    where
        -- hybridization
      parse_basic_sen :: NeSyPatterns -> Maybe (BASIC_SPEC -> AParser st ())
parse_basic_sen NeSyPatterns = (BASIC_SPEC -> AParser st ())
-> Maybe (BASIC_SPEC -> AParser st ())
forall a. a -> Maybe a
Just ((BASIC_SPEC -> AParser st ())
 -> Maybe (BASIC_SPEC -> AParser st ()))
-> (() -> BASIC_SPEC -> AParser st ())
-> ()
-> Maybe (BASIC_SPEC -> AParser st ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AParser st () -> BASIC_SPEC -> AParser st ()
forall a b. a -> b -> a
const (AParser st () -> BASIC_SPEC -> AParser st ())
-> (() -> AParser st ()) -> () -> BASIC_SPEC -> AParser st ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. () -> AParser st ()
forall (m :: * -> *) a. Monad m => a -> m a
return (() -> Maybe (BASIC_SPEC -> AParser st ()))
-> () -> Maybe (BASIC_SPEC -> AParser st ())
forall a b. (a -> b) -> a -> b
$ ()
      stability :: NeSyPatterns -> Stability
stability NeSyPatterns = Stability
Stable
      top_sublogic :: NeSyPatterns -> ()
top_sublogic NeSyPatterns = ()
      all_sublogics :: NeSyPatterns -> [()]
all_sublogics NeSyPatterns = []
      empty_proof_tree :: NeSyPatterns -> ProofTree
empty_proof_tree NeSyPatterns = ProofTree
emptyProofTree
    -- supplied provers
      provers :: NeSyPatterns -> [Prover Sign () Morphism () ProofTree]
provers NeSyPatterns = []
      cons_checkers :: NeSyPatterns -> [ConsChecker Sign () () Morphism ProofTree]
cons_checkers NeSyPatterns = []
      conservativityCheck :: NeSyPatterns -> [ConservativityChecker Sign () Morphism]
conservativityCheck NeSyPatterns = []
      data_logic :: NeSyPatterns -> Maybe AnyLogic
data_logic NeSyPatterns = AnyLogic -> Maybe AnyLogic
forall a. a -> Maybe a
Just (OWL2 -> AnyLogic
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> AnyLogic
Logic OWL2
OWL2)

-- | Static Analysis for propositional logic
instance StaticAnalysis NeSyPatterns
    BASIC_SPEC                -- basic_spec
    ()                   -- sentence
    SYMB_ITEMS                -- symb_items
    SYMB_MAP_ITEMS            -- symb_map_items
    Sign                          -- sign
    Morphism                  -- morphism
    Symbol                      -- symbol
    Symbol                      -- raw_symbol
        where
          basic_analysis :: NeSyPatterns
-> Maybe
     ((BASIC_SPEC, Sign, GlobalAnnos)
      -> Result (BASIC_SPEC, ExtSign Sign Symbol, [Named ()]))
basic_analysis NeSyPatterns =
              ((BASIC_SPEC, Sign, GlobalAnnos)
 -> Result (BASIC_SPEC, ExtSign Sign Symbol, [Named ()]))
-> Maybe
     ((BASIC_SPEC, Sign, GlobalAnnos)
      -> Result (BASIC_SPEC, ExtSign Sign Symbol, [Named ()]))
forall a. a -> Maybe a
Just (BASIC_SPEC, Sign, GlobalAnnos)
-> Result (BASIC_SPEC, ExtSign Sign Symbol, [Named ()])
basicNeSyPatternsAnalysis
          empty_signature :: NeSyPatterns -> Sign
empty_signature NeSyPatterns = Sign
emptySig
          is_subsig :: NeSyPatterns -> Sign -> Sign -> Bool
is_subsig NeSyPatterns = Sign -> Sign -> Bool
isSubSigOf
          subsig_inclusion :: NeSyPatterns -> Sign -> Sign -> Result Morphism
subsig_inclusion NeSyPatterns s :: Sign
s = Morphism -> Result Morphism
forall (m :: * -> *) a. Monad m => a -> m a
return (Morphism -> Result Morphism)
-> (Sign -> Morphism) -> Sign -> Result Morphism
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sign -> Sign -> Morphism
inclusionMap Sign
s
          signature_union :: NeSyPatterns -> Sign -> Sign -> Result Sign
signature_union NeSyPatterns = Sign -> Sign -> Result Sign
sigUnion
          symbol_to_raw :: NeSyPatterns -> Symbol -> Symbol
symbol_to_raw NeSyPatterns = Symbol -> Symbol
symbolToRaw
          id_to_raw :: NeSyPatterns -> Id -> Symbol
id_to_raw NeSyPatterns = Id -> Symbol
idToRaw
          matches :: NeSyPatterns -> Symbol -> Symbol -> Bool
matches NeSyPatterns = Symbol -> Symbol -> Bool
Symbol.matches
          stat_symb_items :: NeSyPatterns -> Sign -> [SYMB_ITEMS] -> Result [Symbol]
stat_symb_items NeSyPatterns = Sign -> [SYMB_ITEMS] -> Result [Symbol]
mkStatSymbItems
          stat_symb_map_items :: NeSyPatterns
-> Sign
-> Maybe Sign
-> [SYMB_MAP_ITEMS]
-> Result (EndoMap Symbol)
stat_symb_map_items NeSyPatterns = Sign -> Maybe Sign -> [SYMB_MAP_ITEMS] -> Result (EndoMap Symbol)
mkStatSymbMapItem
          morphism_union :: NeSyPatterns -> Morphism -> Morphism -> Result Morphism
morphism_union NeSyPatterns = Morphism -> Morphism -> Result Morphism
morphismUnion
          induced_from_morphism :: NeSyPatterns -> EndoMap Symbol -> Sign -> Result Morphism
induced_from_morphism NeSyPatterns = EndoMap Symbol -> Sign -> Result Morphism
inducedFromMorphism
          induced_from_to_morphism :: NeSyPatterns
-> EndoMap Symbol
-> ExtSign Sign Symbol
-> ExtSign Sign Symbol
-> Result Morphism
induced_from_to_morphism NeSyPatterns = EndoMap Symbol
-> ExtSign Sign Symbol -> ExtSign Sign Symbol -> Result Morphism
inducedFromToMorphism
          signature_colimit :: NeSyPatterns
-> Gr Sign (Int, Morphism) -> Result (Sign, Map Int Morphism)
signature_colimit NeSyPatterns = Gr Sign (Int, Morphism) -> Result (Sign, Map Int Morphism)
signatureColimit
#ifdef UNI_PACKAGE
          theory_to_taxonomy :: NeSyPatterns
-> TaxoGraphKind
-> MMiSSOntology
-> Sign
-> [Named ()]
-> Result MMiSSOntology
theory_to_taxonomy NeSyPatterns = TaxoGraphKind
-> MMiSSOntology -> Sign -> [Named ()] -> Result MMiSSOntology
nesy2Tax
#endif

-- | Sublogics