content: {-# 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 Show
  
  instance Language CommonLogic where
      description _ = "CommonLogic (an ISO standard)\n"
  
  instance Category Sign Morphism
      where
        ide = idMor
        dom = source
        cod = target
        isInclusion = Map.null . propMap
        legal_mor = isLegalMorphism
        composeMorphisms = composeMor
  
  instance Sentences CommonLogic
      TEXT_META
      Sign
      Morphism
      Symbol
      where
        negation CommonLogic = Just . negForm
        sym_of CommonLogic = singletonList . symOf
        symmap_of CommonLogic = getSymbolMap -- returns the symbol map
        sym_name CommonLogic = getSymbolName -- returns the name of a symbol
        map_sen CommonLogic = mapSentence -- TODO
        symsOfSen CommonLogic _ = symsOfTextMeta
        symKind CommonLogic = Symbol.symKind
  
  instance Semigroup BASIC_SPEC where
      (Basic_spec l1) <> (Basic_spec l2) = Basic_spec $ l1 ++ l2
  instance Monoid BASIC_SPEC where
      mempty = Basic_spec []
  
  instance Syntax CommonLogic
      BASIC_SPEC
      Symbol
      SYMB_ITEMS
      SYMB_MAP_ITEMS
      where
        parsersAndPrinters CommonLogic =
          addSyntax "KIF" (KIF.basicSpec, Print_KIF.printBasicSpec)
          $ addSyntax "CLIF" (CLIF.basicSpec, pretty)
          $ makeDefault (CLIF.basicSpec, pretty)
        parse_symb_items CommonLogic = Just . const $ CLIF.symbItems
        parse_symb_map_items CommonLogic = Just . const $ 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 = Stable
         all_sublogics CommonLogic = sublogics_all
         empty_proof_tree CommonLogic = emptyProofTree
         provers CommonLogic = []
         omdoc_metatheory CommonLogic = Just clMetaTheory
         export_senToOmdoc CommonLogic = exportSenToOmdoc
         export_symToOmdoc CommonLogic = exportSymToOmdoc
         omdocToSen CommonLogic = OMDocImport.omdocToSen
         omdocToSym CommonLogic = OMDocImport.omdocToSym
  
  
  instance StaticAnalysis CommonLogic
      BASIC_SPEC
      TEXT_META
      SYMB_ITEMS
      SYMB_MAP_ITEMS
      Sign
      Morphism
      Symbol
      Symbol
      where
        basic_analysis CommonLogic = Just basicCommonLogicAnalysis
        empty_signature CommonLogic = emptySig
        is_subsig CommonLogic = isSubSigOf
        subsig_inclusion CommonLogic s = return . inclusionMap s
        signature_union CommonLogic = sigUnion
        symbol_to_raw CommonLogic = symbolToRaw
        id_to_raw CommonLogic = idToRaw
        matches CommonLogic = Symbol.matches
        stat_symb_items CommonLogic _ = mkStatSymbItems
        stat_symb_map_items CommonLogic _ _ = mkStatSymbMapItem
        induced_from_morphism CommonLogic = inducedFromMorphism
        induced_from_to_morphism CommonLogic = inducedFromToMorphism
        add_symb_to_sign CommonLogic = addSymbToSign -- TODO
  
  {-
        stat_symb_items CommonLogic = ()
        stat_symb_map_items CommonLogic = ()
        morphism_union CommonLogic = ()
  -}
        signature_colimit CommonLogic = signColimit
  
  
  -- | Sublogics
  instance SemiLatticeWithTop CommonLogicSL where
      lub = sublogics_max
      top = CommonLogic.Sublogic.top
  
  instance MinSublogic CommonLogicSL BASIC_SPEC where
       minSublogic = sl_basic_spec bottom
  
  instance MinSublogic CommonLogicSL Sign where
      minSublogic = sl_sig bottom
  
  instance SublogicName CommonLogicSL where
      sublogicName = sublogics_name
  
  instance MinSublogic CommonLogicSL TEXT_META where
      minSublogic tm = sublogic_text bottom $ getText tm
  
  instance MinSublogic CommonLogicSL NAME where
      minSublogic = sublogic_name bottom
  
  instance MinSublogic CommonLogicSL Symbol where
      minSublogic = sl_sym bottom
  
  instance MinSublogic CommonLogicSL Morphism where
      minSublogic = sl_mor bottom
  
  instance MinSublogic CommonLogicSL SYMB_MAP_ITEMS where
      minSublogic = sl_symmap bottom
  
  instance MinSublogic CommonLogicSL SYMB_ITEMS where
      minSublogic = sl_symitems bottom
  
  instance ProjectSublogic CommonLogicSL BASIC_SPEC where
    projectSublogic = prBasicSpec
  
  instance ProjectSublogicM CommonLogicSL NAME where
    projectSublogicM = prName
  
  instance ProjectSublogicM CommonLogicSL SYMB_MAP_ITEMS where
    projectSublogicM = prSymMapM
  
  instance ProjectSublogicM CommonLogicSL SYMB_ITEMS where
    projectSublogicM = prSymItemsM
  
  instance ProjectSublogic CommonLogicSL Sign where
    projectSublogic = prSig
  
  instance ProjectSublogic CommonLogicSL Morphism where
    projectSublogic = prMor
  
  instance ProjectSublogicM CommonLogicSL Symbol where
    projectSublogicM = prSymbolM
  