{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances #-}
{- |
Module      :  ./CommonLogic/Logic_CommonLogic.hs
Description :  Instance of class Logic for common logic
Copyright   :  (c) Karl Luc, DFKI Bremen 2010, Eugen Kuksa and Uni Bremen 2011
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  eugenk@informatik.uni-bremen.de
Stability   :  experimental
Portability :  non-portable (imports Logic.Logic)

Instance of class Logic for the common logic
-}

module CommonLogic.Logic_CommonLogic where

import ATC.ProofTree ()

import Common.ProofTree

import CommonLogic.ATC_CommonLogic ()
import CommonLogic.Sign
import CommonLogic.AS_CommonLogic
import CommonLogic.Symbol as Symbol
import CommonLogic.Analysis
import qualified CommonLogic.Parse_CLIF as CLIF
import qualified CommonLogic.Parse_KIF as KIF
import qualified CommonLogic.Print_KIF as Print_KIF
import CommonLogic.Morphism
import CommonLogic.OMDocExport
import CommonLogic.OMDocImport as OMDocImport
import CommonLogic.OMDoc
import CommonLogic.Sublogic

import qualified Data.Map as Map
import Data.Monoid ()

import Logic.Logic

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

instance Language CommonLogic where
    description :: CommonLogic -> String
description _ = "CommonLogic (an ISO standard)\n"

instance Category Sign Morphism
    where
      ide :: Sign -> Morphism
ide = Sign -> Morphism
idMor
      dom :: Morphism -> Sign
dom = Morphism -> Sign
source
      cod :: Morphism -> Sign
cod = Morphism -> Sign
target
      isInclusion :: Morphism -> Bool
isInclusion = Map Id Id -> Bool
forall k a. Map k a -> Bool
Map.null (Map Id Id -> Bool) -> (Morphism -> Map Id Id) -> Morphism -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Morphism -> Map Id Id
propMap
      legal_mor :: Morphism -> Result ()
legal_mor = Morphism -> Result ()
isLegalMorphism
      composeMorphisms :: Morphism -> Morphism -> Result Morphism
composeMorphisms = Morphism -> Morphism -> Result Morphism
composeMor

instance Sentences CommonLogic
    TEXT_META
    Sign
    Morphism
    Symbol
    where
      negation :: CommonLogic -> TEXT_META -> Maybe TEXT_META
negation CommonLogic = TEXT_META -> Maybe TEXT_META
forall a. a -> Maybe a
Just (TEXT_META -> Maybe TEXT_META)
-> (TEXT_META -> TEXT_META) -> TEXT_META -> Maybe TEXT_META
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TEXT_META -> TEXT_META
negForm
      sym_of :: CommonLogic -> Sign -> [Set Symbol]
sym_of CommonLogic = 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
      symmap_of :: CommonLogic -> Morphism -> EndoMap Symbol
symmap_of CommonLogic = Morphism -> EndoMap Symbol
getSymbolMap -- returns the symbol map
      sym_name :: CommonLogic -> Symbol -> Id
sym_name CommonLogic = Symbol -> Id
getSymbolName -- returns the name of a symbol
      map_sen :: CommonLogic -> Morphism -> TEXT_META -> Result TEXT_META
map_sen CommonLogic = Morphism -> TEXT_META -> Result TEXT_META
mapSentence -- TODO
      symsOfSen :: CommonLogic -> Sign -> TEXT_META -> [Symbol]
symsOfSen CommonLogic _ = TEXT_META -> [Symbol]
symsOfTextMeta
      symKind :: CommonLogic -> Symbol -> String
symKind CommonLogic = Symbol -> String
Symbol.symKind

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

instance Syntax CommonLogic
    BASIC_SPEC
    Symbol
    SYMB_ITEMS
    SYMB_MAP_ITEMS
    where
      parsersAndPrinters :: CommonLogic
-> Map
     String (PrefixMap -> AParser st BASIC_SPEC, BASIC_SPEC -> Doc)
parsersAndPrinters CommonLogic =
        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 "KIF" (PrefixMap -> AParser st BASIC_SPEC
forall st. PrefixMap -> AParser st BASIC_SPEC
KIF.basicSpec, BASIC_SPEC -> Doc
Print_KIF.printBasicSpec)
        (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
$ 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 "CLIF" (PrefixMap -> AParser st BASIC_SPEC
forall st. PrefixMap -> AParser st BASIC_SPEC
CLIF.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
CLIF.basicSpec, BASIC_SPEC -> Doc
forall a. Pretty a => a -> Doc
pretty)
      parse_symb_items :: CommonLogic -> Maybe (PrefixMap -> AParser st SYMB_ITEMS)
parse_symb_items CommonLogic = (PrefixMap -> AParser st SYMB_ITEMS)
-> Maybe (PrefixMap -> AParser st SYMB_ITEMS)
forall a. a -> Maybe a
Just ((PrefixMap -> AParser st SYMB_ITEMS)
 -> Maybe (PrefixMap -> AParser st SYMB_ITEMS))
-> (AParser st SYMB_ITEMS -> PrefixMap -> AParser st SYMB_ITEMS)
-> AParser st SYMB_ITEMS
-> Maybe (PrefixMap -> AParser st SYMB_ITEMS)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AParser st SYMB_ITEMS -> PrefixMap -> AParser st SYMB_ITEMS
forall a b. a -> b -> a
const (AParser st SYMB_ITEMS
 -> Maybe (PrefixMap -> AParser st SYMB_ITEMS))
-> AParser st SYMB_ITEMS
-> Maybe (PrefixMap -> AParser st SYMB_ITEMS)
forall a b. (a -> b) -> a -> b
$ AParser st SYMB_ITEMS
forall st. GenParser Char st SYMB_ITEMS
CLIF.symbItems
      parse_symb_map_items :: CommonLogic -> Maybe (PrefixMap -> AParser st SYMB_MAP_ITEMS)
parse_symb_map_items CommonLogic = (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)
 -> Maybe (PrefixMap -> AParser st SYMB_MAP_ITEMS))
-> (AParser st SYMB_MAP_ITEMS
    -> PrefixMap -> AParser st SYMB_MAP_ITEMS)
-> AParser st SYMB_MAP_ITEMS
-> Maybe (PrefixMap -> AParser st SYMB_MAP_ITEMS)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AParser st SYMB_MAP_ITEMS -> PrefixMap -> AParser st SYMB_MAP_ITEMS
forall a b. a -> b -> a
const (AParser st SYMB_MAP_ITEMS
 -> Maybe (PrefixMap -> AParser st SYMB_MAP_ITEMS))
-> AParser st SYMB_MAP_ITEMS
-> Maybe (PrefixMap -> AParser st SYMB_MAP_ITEMS)
forall a b. (a -> b) -> a -> b
$ AParser st SYMB_MAP_ITEMS
forall st. GenParser Char st SYMB_MAP_ITEMS
CLIF.symbMapItems

instance Logic CommonLogic
    CommonLogicSL     -- Sublogics
    BASIC_SPEC        -- basic_spec
    TEXT_META         -- sentence
    SYMB_ITEMS        -- symb_items
    SYMB_MAP_ITEMS    -- symb_map_items
    Sign              -- sign
    Morphism          -- morphism
    Symbol            -- symbol
    Symbol            -- raw_symbol
    ProofTree         -- proof_tree
    where
       stability :: CommonLogic -> Stability
stability CommonLogic = Stability
Stable
       all_sublogics :: CommonLogic -> [CommonLogicSL]
all_sublogics CommonLogic = [CommonLogicSL]
sublogics_all
       empty_proof_tree :: CommonLogic -> ProofTree
empty_proof_tree CommonLogic = ProofTree
emptyProofTree
       provers :: CommonLogic
-> [Prover Sign TEXT_META Morphism CommonLogicSL ProofTree]
provers CommonLogic = []
       omdoc_metatheory :: CommonLogic -> Maybe OMCD
omdoc_metatheory CommonLogic = OMCD -> Maybe OMCD
forall a. a -> Maybe a
Just OMCD
clMetaTheory
       export_senToOmdoc :: CommonLogic -> NameMap Symbol -> TEXT_META -> Result TCorOMElement
export_senToOmdoc CommonLogic = NameMap Symbol -> TEXT_META -> Result TCorOMElement
exportSenToOmdoc
       export_symToOmdoc :: CommonLogic
-> NameMap Symbol -> Symbol -> String -> Result TCElement
export_symToOmdoc CommonLogic = NameMap Symbol -> Symbol -> String -> Result TCElement
exportSymToOmdoc
       omdocToSen :: CommonLogic
-> SigMapI Symbol
-> TCElement
-> String
-> Result (Maybe (Named TEXT_META))
omdocToSen CommonLogic = SigMapI Symbol
-> TCElement -> String -> Result (Maybe (Named TEXT_META))
OMDocImport.omdocToSen
       omdocToSym :: CommonLogic
-> SigMapI Symbol -> TCElement -> String -> Result Symbol
omdocToSym CommonLogic = SigMapI Symbol -> TCElement -> String -> Result Symbol
OMDocImport.omdocToSym


instance StaticAnalysis CommonLogic
    BASIC_SPEC
    TEXT_META
    SYMB_ITEMS
    SYMB_MAP_ITEMS
    Sign
    Morphism
    Symbol
    Symbol
    where
      basic_analysis :: CommonLogic
-> Maybe
     ((BASIC_SPEC, Sign, GlobalAnnos)
      -> Result (BASIC_SPEC, ExtSign Sign Symbol, [Named TEXT_META]))
basic_analysis CommonLogic = ((BASIC_SPEC, Sign, GlobalAnnos)
 -> Result (BASIC_SPEC, ExtSign Sign Symbol, [Named TEXT_META]))
-> Maybe
     ((BASIC_SPEC, Sign, GlobalAnnos)
      -> Result (BASIC_SPEC, ExtSign Sign Symbol, [Named TEXT_META]))
forall a. a -> Maybe a
Just (BASIC_SPEC, Sign, GlobalAnnos)
-> Result (BASIC_SPEC, ExtSign Sign Symbol, [Named TEXT_META])
basicCommonLogicAnalysis
      empty_signature :: CommonLogic -> Sign
empty_signature CommonLogic = Sign
emptySig
      is_subsig :: CommonLogic -> Sign -> Sign -> Bool
is_subsig CommonLogic = Sign -> Sign -> Bool
isSubSigOf
      subsig_inclusion :: CommonLogic -> Sign -> Sign -> Result Morphism
subsig_inclusion CommonLogic 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 :: CommonLogic -> Sign -> Sign -> Result Sign
signature_union CommonLogic = Sign -> Sign -> Result Sign
sigUnion
      symbol_to_raw :: CommonLogic -> Symbol -> Symbol
symbol_to_raw CommonLogic = Symbol -> Symbol
symbolToRaw
      id_to_raw :: CommonLogic -> Id -> Symbol
id_to_raw CommonLogic = Id -> Symbol
idToRaw
      matches :: CommonLogic -> Symbol -> Symbol -> Bool
matches CommonLogic = Symbol -> Symbol -> Bool
Symbol.matches
      stat_symb_items :: CommonLogic -> Sign -> [SYMB_ITEMS] -> Result [Symbol]
stat_symb_items CommonLogic _ = [SYMB_ITEMS] -> Result [Symbol]
mkStatSymbItems
      stat_symb_map_items :: CommonLogic
-> Sign
-> Maybe Sign
-> [SYMB_MAP_ITEMS]
-> Result (EndoMap Symbol)
stat_symb_map_items CommonLogic _ _ = [SYMB_MAP_ITEMS] -> Result (EndoMap Symbol)
mkStatSymbMapItem
      induced_from_morphism :: CommonLogic -> EndoMap Symbol -> Sign -> Result Morphism
induced_from_morphism CommonLogic = EndoMap Symbol -> Sign -> Result Morphism
inducedFromMorphism
      induced_from_to_morphism :: CommonLogic
-> EndoMap Symbol
-> ExtSign Sign Symbol
-> ExtSign Sign Symbol
-> Result Morphism
induced_from_to_morphism CommonLogic = EndoMap Symbol
-> ExtSign Sign Symbol -> ExtSign Sign Symbol -> Result Morphism
inducedFromToMorphism
      add_symb_to_sign :: CommonLogic -> Sign -> Symbol -> Result Sign
add_symb_to_sign CommonLogic = Sign -> Symbol -> Result Sign
addSymbToSign -- TODO

{-
      stat_symb_items CommonLogic = ()
      stat_symb_map_items CommonLogic = ()
      morphism_union CommonLogic = ()
-}
      signature_colimit :: CommonLogic
-> Gr Sign (Int, Morphism) -> Result (Sign, Map Int Morphism)
signature_colimit CommonLogic = Gr Sign (Int, Morphism) -> Result (Sign, Map Int Morphism)
signColimit


-- | Sublogics
instance SemiLatticeWithTop CommonLogicSL where
    lub :: CommonLogicSL -> CommonLogicSL -> CommonLogicSL
lub = CommonLogicSL -> CommonLogicSL -> CommonLogicSL
sublogics_max
    top :: CommonLogicSL
top = CommonLogicSL
CommonLogic.Sublogic.top

instance MinSublogic CommonLogicSL BASIC_SPEC where
     minSublogic :: BASIC_SPEC -> CommonLogicSL
minSublogic = CommonLogicSL -> BASIC_SPEC -> CommonLogicSL
sl_basic_spec CommonLogicSL
bottom

instance MinSublogic CommonLogicSL Sign where
    minSublogic :: Sign -> CommonLogicSL
minSublogic = CommonLogicSL -> Sign -> CommonLogicSL
sl_sig CommonLogicSL
bottom

instance SublogicName CommonLogicSL where
    sublogicName :: CommonLogicSL -> String
sublogicName = CommonLogicSL -> String
sublogics_name

instance MinSublogic CommonLogicSL TEXT_META where
    minSublogic :: TEXT_META -> CommonLogicSL
minSublogic tm :: TEXT_META
tm = CommonLogicSL -> TEXT -> CommonLogicSL
sublogic_text CommonLogicSL
bottom (TEXT -> CommonLogicSL) -> TEXT -> CommonLogicSL
forall a b. (a -> b) -> a -> b
$ TEXT_META -> TEXT
getText TEXT_META
tm

instance MinSublogic CommonLogicSL NAME where
    minSublogic :: SIMPLE_ID -> CommonLogicSL
minSublogic = CommonLogicSL -> SIMPLE_ID -> CommonLogicSL
sublogic_name CommonLogicSL
bottom

instance MinSublogic CommonLogicSL Symbol where
    minSublogic :: Symbol -> CommonLogicSL
minSublogic = CommonLogicSL -> Symbol -> CommonLogicSL
sl_sym CommonLogicSL
bottom

instance MinSublogic CommonLogicSL Morphism where
    minSublogic :: Morphism -> CommonLogicSL
minSublogic = CommonLogicSL -> Morphism -> CommonLogicSL
sl_mor CommonLogicSL
bottom

instance MinSublogic CommonLogicSL SYMB_MAP_ITEMS where
    minSublogic :: SYMB_MAP_ITEMS -> CommonLogicSL
minSublogic = CommonLogicSL -> SYMB_MAP_ITEMS -> CommonLogicSL
sl_symmap CommonLogicSL
bottom

instance MinSublogic CommonLogicSL SYMB_ITEMS where
    minSublogic :: SYMB_ITEMS -> CommonLogicSL
minSublogic = CommonLogicSL -> SYMB_ITEMS -> CommonLogicSL
sl_symitems CommonLogicSL
bottom

instance ProjectSublogic CommonLogicSL BASIC_SPEC where
  projectSublogic :: CommonLogicSL -> BASIC_SPEC -> BASIC_SPEC
projectSublogic = CommonLogicSL -> BASIC_SPEC -> BASIC_SPEC
prBasicSpec

instance ProjectSublogicM CommonLogicSL NAME where
  projectSublogicM :: CommonLogicSL -> SIMPLE_ID -> Maybe SIMPLE_ID
projectSublogicM = CommonLogicSL -> SIMPLE_ID -> Maybe SIMPLE_ID
prName

instance ProjectSublogicM CommonLogicSL SYMB_MAP_ITEMS where
  projectSublogicM :: CommonLogicSL -> SYMB_MAP_ITEMS -> Maybe SYMB_MAP_ITEMS
projectSublogicM = CommonLogicSL -> SYMB_MAP_ITEMS -> Maybe SYMB_MAP_ITEMS
prSymMapM

instance ProjectSublogicM CommonLogicSL SYMB_ITEMS where
  projectSublogicM :: CommonLogicSL -> SYMB_ITEMS -> Maybe SYMB_ITEMS
projectSublogicM = CommonLogicSL -> SYMB_ITEMS -> Maybe SYMB_ITEMS
prSymItemsM

instance ProjectSublogic CommonLogicSL Sign where
  projectSublogic :: CommonLogicSL -> Sign -> Sign
projectSublogic = CommonLogicSL -> Sign -> Sign
prSig

instance ProjectSublogic CommonLogicSL Morphism where
  projectSublogic :: CommonLogicSL -> Morphism -> Morphism
projectSublogic = CommonLogicSL -> Morphism -> Morphism
prMor

instance ProjectSublogicM CommonLogicSL Symbol where
  projectSublogicM :: CommonLogicSL -> Symbol -> Maybe Symbol
projectSublogicM = CommonLogicSL -> Symbol -> Maybe Symbol
prSymbolM