hets/ExtModal/Logic_ExtModal.hs

	Logic_ExtModal.hs revision 8b52f992f2f7a0c4fa6e3692cf868a6baadaa69b
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances #-}
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa{- |
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen KuksaModule      :  $Header$
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen KuksaDescription :  Instance of class Logic for ExtModal
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen KuksaCopyright   :  DFKI GmbH 2009
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen KuksaLicense     :  GPLv2 or higher, see LICENSE.txt
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen KuksaMaintainer  :  codruta.liliana@gmail.com
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen KuksaStability   :  experimental
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen KuksaPortability :  non-portable (imports Logic)
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen KuksaInstance of class Logic for ExtModal
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa-}
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksamodule ExtModal.Logic_ExtModal where
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksaimport ExtModal.AS_ExtModal
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksaimport ExtModal.ExtModalSign
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksaimport ExtModal.ATC_ExtModal()
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksaimport ExtModal.Parse_AS
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksaimport ExtModal.Print_AS
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksaimport ExtModal.StatAna
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksaimport ExtModal.MorphismExtension
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksaimport CASL.Sign
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksaimport CASL.Morphism
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksaimport CASL.SymbolMapAnalysis
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksaimport CASL.AS_Basic_CASL
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksaimport CASL.Parse_AS_Basic
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksaimport CASL.MapSentence
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksaimport CASL.SymbolParser
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksaimport CASL.SimplifySen
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksaimport CASL.Taxonomy
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksaimport CASL.Logic_CASL ()
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksaimport Logic.Logic
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksaimport qualified Data.Map as Map
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksadata ExtModal = ExtModal deriving Show
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksainstance Language ExtModal where
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa        description _ = unlines
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa         [ "ExtModal is the 'extended modal logic' extension of CASL. "
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa         , "Syntax for ordinary modalities, multi-modal logic, dynamic "
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa         , "logic, graded modal logic, hybrid logic, CTL* and mu-calculus  "
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa         , "is provided. Specific modal logics can be optained via "
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa         , "restrictions to sublanguages."
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa         ]
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksatype ExtModalSign = Sign EM_FORMULA EModalSign
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksatype ExtModalMorph = Morphism EM_FORMULA EModalSign MorphExtension
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksatype ExtModalFORMULA = FORMULA EM_FORMULA
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksainstance SignExtension EModalSign where
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa        isSubSignExtension = isSubEModalSign
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksainstance Syntax ExtModal EM_BASIC_SPEC SYMB_ITEMS SYMB_MAP_ITEMS where
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa        parse_basic_spec ExtModal = Just $ basicSpec ext_modal_reserved_words
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa        parse_symb_items ExtModal = Just $ symbItems ext_modal_reserved_words
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa        parse_symb_map_items ExtModal =
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa            Just $ symbMapItems ext_modal_reserved_words
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa-- Modal formula mapping via signature morphism
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksamap_EM_FORMULA :: MapSen EM_FORMULA EModalSign MorphExtension
map_EM_FORMULA morph (BoxOrDiamond choice t_m leq_geq number f pos) =
  let new_tm tm = case tm of
        Simple_modality sm ->
            let mds = mod_map (extended_map morph) in
            if Map.member sm mds then Simple_modality (mds Map.! sm) else tm
        Composition tm1 tm2 -> Composition (new_tm tm1) (new_tm tm2)
        Union tm1 tm2 -> Union (new_tm tm1) (new_tm tm2)
        TransitiveClosure tm1 -> TransitiveClosure (new_tm tm1)
        Guard frm -> Guard (mapSen map_EM_FORMULA morph frm)
      new_f = mapSen map_EM_FORMULA morph f
  in BoxOrDiamond choice (new_tm t_m) leq_geq number new_f pos


map_EM_FORMULA morph (Hybrid choice nm f pos) =
  let new_nom = case nm of
        Nominal nom -> let nms = nom_map (extended_map morph) in
          if Map.member nom nms then Nominal (nms Map.! nom) else nm
      new_f = mapSen map_EM_FORMULA morph f
  in Hybrid choice new_nom new_f pos


map_EM_FORMULA morph (UntilSince choice f1 f2 pos) =
        let new_f1 = mapSen map_EM_FORMULA morph f1
            new_f2 = mapSen map_EM_FORMULA morph f2
        in UntilSince choice new_f1 new_f2 pos

map_EM_FORMULA morph (NextY choice f pos) =
        let new_f = mapSen map_EM_FORMULA morph f
        in NextY choice new_f pos

map_EM_FORMULA morph (PathQuantification choice f pos) =
        let new_f = mapSen map_EM_FORMULA morph f
        in PathQuantification choice new_f pos

map_EM_FORMULA morph (StateQuantification t_dir choice f pos) =
        let new_f = mapSen map_EM_FORMULA morph f
        in StateQuantification t_dir choice new_f pos

map_EM_FORMULA morph (FixedPoint choice p_var f pos) =
        let new_f = mapSen map_EM_FORMULA morph f
        in FixedPoint choice p_var new_f pos

-- Simplification of formulas - simplifySen for ExtFORMULA
simEMSen :: Sign EM_FORMULA EModalSign -> EM_FORMULA -> EM_FORMULA
simEMSen sign (BoxOrDiamond choice tm leq_geq number f pos) =
        BoxOrDiamond choice tm leq_geq number
            (simplifySen frmTypeAna simEMSen sign f) pos
simEMSen sign (Hybrid choice nom f pos) =
        Hybrid choice nom (simplifySen frmTypeAna simEMSen sign f) pos
simEMSen sign (UntilSince choice f1 f2 pos) =
        UntilSince choice (simplifySen frmTypeAna simEMSen sign f1)
                (simplifySen frmTypeAna simEMSen sign f2) pos
simEMSen sign (NextY choice f pos) =
        NextY choice (simplifySen frmTypeAna simEMSen sign f) pos
simEMSen sign (PathQuantification choice f pos) =
        PathQuantification choice (simplifySen frmTypeAna simEMSen sign f) pos
simEMSen sign (StateQuantification t_dir choice f pos) =
        StateQuantification t_dir choice
            (simplifySen frmTypeAna simEMSen sign f) pos
simEMSen sign (FixedPoint choice p_var f pos) =
        FixedPoint choice p_var (simplifySen frmTypeAna simEMSen sign f) pos

instance Sentences ExtModal ExtModalFORMULA ExtModalSign ExtModalMorph Symbol
    where
        map_sen ExtModal morph = return . mapSen map_EM_FORMULA morph
        simplify_sen ExtModal = simplifySen frmTypeAna simEMSen
        print_sign ExtModal sig = printSign
                (printEModalSign $ simplifySen frmTypeAna simEMSen sig) sig
        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
        final_union ExtModal = finalUnion addEModalSign
        morphism_union ExtModal = morphismUnion (const id) addEModalSign
        is_subsig ExtModal = isSubSig isSubEModalSign
        subsig_inclusion ExtModal = sigInclusion emptyMorphExtension
        generated_sign ExtModal = generatedSign emptyMorphExtension
        cogenerated_sign ExtModal = cogeneratedSign emptyMorphExtension
        induced_from_morphism ExtModal = inducedFromMorphism emptyMorphExtension
        induced_from_to_morphism ExtModal =
          inducedFromToMorphism emptyMorphExtension isSubEModalSign
            diffEModalSign
        theory_to_taxonomy ExtModal = convTaxo

instance Logic ExtModal () EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS
    SYMB_MAP_ITEMS ExtModalSign ExtModalMorph Symbol RawSymbol () where
        stability _ = Experimental
        empty_proof_tree _ = ()