{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}
{- |
Module      :  ./CSL/Logic_CSL.hs
Description :  Instance of class Logic for CSL
Copyright   :  (c) Dominik Dietrich, DFKI Bremen 2010
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  dominik.dietrich@dfki.de
Stability   :  experimental
Portability :  non-portable (imports Logic.Logic)

Instance of class Logic for the CSL logic
   Also the instances for Syntax and Category.
-}


module CSL.Logic_CSL where

import ATC.ProofTree ()

import CSL.AS_BASIC_CSL
import CSL.ATC_CSL ()
import CSL.Analysis
import CSL.Morphism
import CSL.Parse_AS_Basic
import CSL.ReduceProve
import CSL.Sign
import CSL.Symbol
import CSL.Tools

import qualified Data.Map as Map
import Data.Monoid

import Logic.Logic

-- | Lid for reduce logic
data CSL = CSL

instance Show CSL where
    show _ = "EnCL"

instance Language CSL where
    description _ = "EnCL Logic\n"
-- language_name _ = "EnCL"

-- | Instance of Category for CSL logic
instance Category Sign Morphism where
    -- Identity morhpism
    ide = idMor
    -- Returns the domain of a morphism
    dom = source
    -- Returns the codomain of a morphism
    cod = target
    -- check if morphism is inclusion
    isInclusion = Map.null . operatorMap
    -- composition of morphisms
    composeMorphisms = composeMor

-- | Instance of Sentences for reduce logic
instance Sentences CSL CMD
    Sign Morphism Symbol where
    negation CSL = Just . negateFormula
    -- returns the set of symbols --> including operators
    sym_of CSL = singletonList . symOf
    {- returns the symbol map -->
    the internal map only contains changes but the external symbol map
    must also contain identity mappings for all remaining symbols -}
    symmap_of CSL = getSymbolMap
    -- returns the name of a symbol --> id
    sym_name CSL = getSymbolName
    {- translation of sentences along signature morphism -->
    rename the used operators according to the morphism -}
    map_sen CSL = mapSentence
    -- there is nothing to leave out
    simplify_sen CSL _ = id

instance Monoid BASIC_SPEC where
    mempty = Basic_spec []
    mappend (Basic_spec l1) (Basic_spec l2) = Basic_spec $ l1 ++ l2

-- | Syntax of CSL logic
instance Syntax CSL BASIC_SPEC Symbol
    SYMB_ITEMS SYMB_MAP_ITEMS where
         parse_basic_spec CSL = parseBasicSpec
         parse_symb_items CSL = parseSymbItems
         parse_symb_map_items CSL = parseSymbMapItems

-- | Instance of Logic for reduce logc
instance Logic CSL
    ()                        -- Sublogics
    BASIC_SPEC                -- basic_spec
    CMD                       -- sentences are CAS commands
    SYMB_ITEMS                -- symb_items
    SYMB_MAP_ITEMS            -- symb_map_items
    Sign                      -- sign
    Morphism                  -- morphism
    Symbol                    -- symbol
    Symbol                    -- raw_symbol
    [EXPRESSION]              -- proof_tree
    where
      stability CSL = Experimental
      empty_proof_tree CSL = []
      -- supplied provers
      provers CSL = [reduceProver]

-- | Static Analysis for reduce logic
instance StaticAnalysis CSL
    BASIC_SPEC                -- basic_spec
    CMD                       -- sentence
    SYMB_ITEMS                -- symb_items
    SYMB_MAP_ITEMS            -- symb_map_items
    Sign                      -- sign
    Morphism                  -- morphism
    Symbol                    -- symbol
    Symbol                    -- raw_symbol
        where
          basic_analysis CSL = Just basicCSLAnalysis
          empty_signature CSL = emptySig
          is_subsig CSL = isSubSigOf
          subsig_inclusion CSL s = return . inclusionMap s
          signature_union CSL = sigUnion
          symbol_to_raw CSL = symbolToRaw
          id_to_raw CSL = idToRaw
{- matches       CSL            = Symbol.matches
stat_symb_items CSL          = mkStatSymbItems
stat_symb_map_items CSL      = mkStatSymbMapItem -}
          morphism_union CSL = morphismUnion
{- induced_from_morphism CSL    = inducedFromMorphism
induced_from_to_morphism CSL = inducedFromToMorphism -}
