{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}

{- |

Module : ./ExtModal/Logic_ExtModal.hs

Description : Instance of class Logic for ExtModal

Copyright : DFKI GmbH 2009

License : GPLv2 or higher, see LICENSE.txt

Maintainer : Christian.Maeder@dfki.de

Stability : experimental

Portability : non-portable (imports Logic)

Instance of class Logic for ExtModal

-}

module ExtModal.Logic_ExtModal where

import ExtModal.AS_ExtModal

import ExtModal.ExtModalSign

import ExtModal.ATC_ExtModal ()

import ExtModal.Parse_AS

import ExtModal.StatAna

import ExtModal.MorphismExtension

import ExtModal.Sublogic

import CASL.AS_Basic_CASL

import CASL.Logic_CASL

import CASL.MapSentence

import CASL.Morphism

import CASL.Parse_AS_Basic

import CASL.Sign

import CASL.SimplifySen

import CASL.Sublogic

import CASL.SymbolMapAnalysis

import CASL.SymbolParser

import CASL.Taxonomy

import CASL.ToDoc

import Logic.Logic

import Common.DocUtils

import qualified Common.Lib.MapSet as MapSet

import qualified Data.Set as Set

data ExtModal = ExtModal deriving Show

instance Language ExtModal where

description _ = unlines

[ "ExtModal is the 'extended modal logic' extension of CASL. "

, "Syntax for ordinary modalities, multi-modal logic, dynamic "

, "logic, graded modal logic, hybrid logic, CTL* and mu-calculus "

, "is provided. Specific modal logics can be obtained via "

, "restrictions to sublanguages."

]

type ExtModalSign = Sign EM_FORMULA EModalSign

type ExtModalMorph = Morphism EM_FORMULA EModalSign MorphExtension

type ExtModalFORMULA = FORMULA EM_FORMULA

instance SignExtension EModalSign where

isSubSignExtension = isSubEModalSign

instance Syntax ExtModal EM_BASIC_SPEC Symbol SYMB_ITEMS SYMB_MAP_ITEMS where

parse_basic_spec ExtModal = Just $ basicSpec ext_modal_reserved_words

parse_symb_items ExtModal = Just $ symbItems ext_modal_reserved_words

parse_symb_map_items ExtModal =

Just $ symbMapItems ext_modal_reserved_words

-- Simplification of formulas - simplifySen for ExtFORMULA

simEMSen :: Sign EM_FORMULA EModalSign -> EM_FORMULA -> EM_FORMULA

simEMSen sign = mapExtForm (simplifySen frmTypeAna simEMSen sign)

correctTarget :: Morphism f EModalSign m -> Morphism f EModalSign m

correctTarget m = m

{ mtarget = correctSign $ mtarget m

, msource = correctSign $ msource m }

instance Sentences ExtModal ExtModalFORMULA ExtModalSign ExtModalMorph Symbol

where

map_sen ExtModal morph = return . mapSen mapEMform morph

simplify_sen ExtModal = simplifySen frmTypeAna simEMSen . setRevSortRel

print_named ExtModal = printTheoryFormula

print_sign ExtModal sig = let e = extendedInfo sig in pretty sig

{ opMap = diffOpMapSet (opMap sig) $ flexOps e

, predMap = Set.fold (`MapSet.delete` nomPType)

(diffMapSet (predMap sig) $ flexPreds e) $ nominals e

}

sym_of ExtModal = symOf

symmap_of ExtModal = morphismToSymbMap

sym_name ExtModal = symName

instance StaticAnalysis ExtModal EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS

SYMB_MAP_ITEMS ExtModalSign ExtModalMorph Symbol RawSymbol where

basic_analysis ExtModal = Just basicEModalAnalysis

stat_symb_map_items ExtModal = statSymbMapItems

stat_symb_items ExtModal = statSymbItems

symbol_to_raw ExtModal = symbolToRaw

id_to_raw ExtModal = idToRaw

matches ExtModal = CASL.Morphism.matches

empty_signature ExtModal = emptySign emptyEModalSign

signature_union ExtModal sgn = return . addSig addEModalSign sgn

intersection ExtModal sgn = return . interSig interEModalSign sgn

signatureDiff ExtModal sgn = return . diffSig diffEModalSign sgn

final_union ExtModal = finalUnion addEModalSign

morphism_union ExtModal = plainMorphismUnion addEModalSign

is_subsig ExtModal = isSubSig isSubEModalSign

subsig_inclusion ExtModal = sigInclusion emptyMorphExtension

generated_sign ExtModal s = fmap correctTarget

. generatedSign emptyMorphExtension s

cogenerated_sign ExtModal s = fmap correctTarget

. cogeneratedSign emptyMorphExtension s

induced_from_morphism ExtModal =

inducedFromMorphismExt inducedEMsign

(constMorphExt emptyMorphExtension)

induced_from_to_morphism ExtModal =

inducedFromToMorphismExt inducedEMsign

(constMorphExt emptyMorphExtension)

(\ _ _ -> return emptyMorphExtension) isSubEModalSign diffEModalSign

theory_to_taxonomy ExtModal = convTaxo

instance Logic ExtModal ExtModalSL EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS

SYMB_MAP_ITEMS ExtModalSign ExtModalMorph Symbol RawSymbol () where

stability ExtModal = Experimental

all_sublogics ExtModal = sublogics_all $ foleml : concat sublogicsDim

sublogicDimensions ExtModal = sDims sublogicsDim

parseSublogic ExtModal = parseSL $ Just . parseSublog

empty_proof_tree ExtModal = ()

instance MinSL Sublogic EM_FORMULA where

minSL = minSublogicOfEM

instance ProjForm Sublogic EM_FORMULA where

projForm _ = Just . ExtFORMULA

instance ProjSigItem Sublogic EM_SIG_ITEM EM_FORMULA where

projSigItems _ s = (Just $ Ext_SIG_ITEMS s, [])

instance ProjBasic Sublogic EM_BASIC_ITEM EM_SIG_ITEM EM_FORMULA where

projBasicItems _ b = (Just $ Ext_BASIC_ITEMS b, [])

instance MinSL Sublogic EM_SIG_ITEM where

minSL = comp_list . minSLExtSigItem

instance MinSL Sublogic EM_BASIC_ITEM where

minSL = minSublogicEMBasic

instance MinSL Sublogic EModalSign where

minSL = minSublogicEMSign

instance NameSL Sublogic where

nameSL = sublogName