Logic_VSE.hs revision d5833d2ee7bafcbf2fdd2bdfd9a728c769b100c7
876bd2c70a93981cc80f8376284616bce4a0fefcChristian Maeder{-# LANGUAGE CPP, MultiParamTypeClasses, TypeSynonymInstances #-}
e6d40133bc9f858308654afb1262b8b483ec5922Till MossakowskiModule : $Header$
999434073eb1711d8db3a72a6405d86546553851Christian MaederDescription : the incomplete Logic instance for VSE
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuCopyright : (c) C. Maeder, DFKI 2008
9af1cee46dd16ba0c55a904a9d21ee2200bca2aeMingyi LiuLicense : GPLv2 or higher, see LICENSE.txt
cd2265c1c7279c901e34383275e0ca44a11d5d6cMingyi LiuMaintainer : Christian.Maeder@dfki.de
cd2265c1c7279c901e34383275e0ca44a11d5d6cMingyi LiuStability : provisional
9af1cee46dd16ba0c55a904a9d21ee2200bca2aeMingyi LiuPortability : non-portable (via Logic.Logic)
9af1cee46dd16ba0c55a904a9d21ee2200bca2aeMingyi Liumorphisms and symbols need to be extended, too
2568e0db076fe349a5d609e0458ac0c3ee6a641cChristian Maederimport CASL.Logic_CASL () -- instance Category VSESign VSEMor
3f540ec9f3d4356f7fe85a699f21bfe7f0e9e70eMingyi Liu#ifdef UNI_PACKAGE
a739d7d8d0ce89e88af5ed6eb3379e9a295271c8Christian Maederimport qualified Data.Map as Map
492287e5f5e91783ee5e169f773f28cafe93a3a9Mingyi Liudata VSE = VSE deriving Show
2568e0db076fe349a5d609e0458ac0c3ee6a641cChristian Maederinstance Language VSE where
2568e0db076fe349a5d609e0458ac0c3ee6a641cChristian Maeder description _ =
2568e0db076fe349a5d609e0458ac0c3ee6a641cChristian Maeder "VSE extends CASL by modal operators and programs."
2568e0db076fe349a5d609e0458ac0c3ee6a641cChristian Maederinstance SignExtension Procs where
2568e0db076fe349a5d609e0458ac0c3ee6a641cChristian Maeder isSubSignExtension = isSubProcsMap
619b330c90b31f5f269c0bbecfee7c7380bdc40bMingyi Liuinstance Syntax VSE VSEBasicSpec SYMB_ITEMS SYMB_MAP_ITEMS where
6f449482b2ca9189ac5fe5d3b2e1cb8de6e10cbcMarkus Gross parse_basic_spec VSE = Just $ basicSpec reservedWords
2568e0db076fe349a5d609e0458ac0c3ee6a641cChristian Maeder parse_symb_items VSE = Just $ symbItems reservedWords
2568e0db076fe349a5d609e0458ac0c3ee6a641cChristian Maeder parse_symb_map_items VSE = Just $ symbMapItems reservedWords
2568e0db076fe349a5d609e0458ac0c3ee6a641cChristian Maederinstance Sentences VSE Sentence VSESign VSEMor Symbol where
2568e0db076fe349a5d609e0458ac0c3ee6a641cChristian Maeder map_sen VSE m = return . mapSen mapDlformula m
2568e0db076fe349a5d609e0458ac0c3ee6a641cChristian Maeder sym_of VSE = symOf
2568e0db076fe349a5d609e0458ac0c3ee6a641cChristian Maeder symmap_of VSE = morphismToSymbMap
6d2309933b2046cbbe6d059e9393fa8c54271f51Mingyi Liu sym_name VSE = symName
ae1a23353330c7438cd1114e3bade7782999db93Mingyi Liu simplify_sen VSE = simplifySen minExpForm simpDlformula
ae1a23353330c7438cd1114e3bade7782999db93Mingyi Liu print_named VSE = printTheoryFormula
ae1a23353330c7438cd1114e3bade7782999db93Mingyi Liu print_sign VSE sig = let e = extendedInfo sig in
2568e0db076fe349a5d609e0458ac0c3ee6a641cChristian Maeder pretty sig { opMap = diffOpMapSet (opMap sig) $ procsToOpMap e
2568e0db076fe349a5d609e0458ac0c3ee6a641cChristian Maeder , predMap = diffMapSet (predMap sig) $ procsToPredMap e }
2568e0db076fe349a5d609e0458ac0c3ee6a641cChristian MaederinterSigM :: Monad m => (e -> e -> m e) -> Sign f e -> Sign f e -> m (Sign f e)
2568e0db076fe349a5d609e0458ac0c3ee6a641cChristian MaederinterSigM f a b = do
2568e0db076fe349a5d609e0458ac0c3ee6a641cChristian Maeder e <- f (extendedInfo a) $ extendedInfo b
ae1a23353330c7438cd1114e3bade7782999db93Mingyi Liu return $ interSig (const $ const e) a b
a1e89617afa7366f5a5319b13833b1f08bcb72f0Mingyi Liuinstance StaticAnalysis VSE VSEBasicSpec Sentence
a1e89617afa7366f5a5319b13833b1f08bcb72f0Mingyi Liu SYMB_ITEMS SYMB_MAP_ITEMS
2568e0db076fe349a5d609e0458ac0c3ee6a641cChristian Maeder Symbol RawSymbol where
2568e0db076fe349a5d609e0458ac0c3ee6a641cChristian Maeder basic_analysis VSE = Just basicAna
2568e0db076fe349a5d609e0458ac0c3ee6a641cChristian Maeder stat_symb_map_items VSE _ = statSymbMapItems
a1e89617afa7366f5a5319b13833b1f08bcb72f0Mingyi Liu stat_symb_items VSE _ = statSymbItems
96a3f4b391a98d0e91bc1f608398442f29d4c69ecmaeder signature_colimit VSE diag =
96a3f4b391a98d0e91bc1f608398442f29d4c69ecmaeder let (sig, mmor) = signColimit diag extVSEColimit
bf28fda4cb91c15978baf8543314642f46c3476ccmaeder in return (correctSign sig, Map.map correctTarget mmor)
bf28fda4cb91c15978baf8543314642f46c3476ccmaeder qualify VSE = qualifySigExt inducedExt emptyMorExt
96a3f4b391a98d0e91bc1f608398442f29d4c69ecmaeder symbol_to_raw VSE = symbolToRaw
96a3f4b391a98d0e91bc1f608398442f29d4c69ecmaeder id_to_raw VSE = idToRaw
a739d7d8d0ce89e88af5ed6eb3379e9a295271c8Christian Maeder empty_signature VSE = emptySign emptyProcs
2568e0db076fe349a5d609e0458ac0c3ee6a641cChristian Maeder signature_union VSE = addSigM unionProcs
2568e0db076fe349a5d609e0458ac0c3ee6a641cChristian Maeder intersection VSE = interSigM interProcs
9af1cee46dd16ba0c55a904a9d21ee2200bca2aeMingyi Liu morphism_union VSE = morphismUnionM (const id) unionProcs
3c09bbecb4752cc78bd3eb8938099fd0c32b42b7Mingyi Liu final_union VSE = addSigM unionProcs
9a7e1781e935fea3b9b296fd9593e3ead8738413Markus Gross is_subsig VSE = isSubSig isSubProcsMap
a739d7d8d0ce89e88af5ed6eb3379e9a295271c8Christian Maeder subsig_inclusion VSE = sigInclusion emptyMorExt
2568e0db076fe349a5d609e0458ac0c3ee6a641cChristian Maeder cogenerated_sign VSE s = fmap correctTarget
2568e0db076fe349a5d609e0458ac0c3ee6a641cChristian Maeder . cogeneratedSign emptyMorExt s
2568e0db076fe349a5d609e0458ac0c3ee6a641cChristian Maeder generated_sign VSE s = fmap correctTarget
9af1cee46dd16ba0c55a904a9d21ee2200bca2aeMingyi Liu . generatedSign emptyMorExt s
5dc710d31ab42ee0eaec4689c7797cb7a43d190cMingyi Liu induced_from_morphism VSE rm = fmap correctTarget
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder . inducedFromMorphismExt inducedExt (constMorphExt emptyMorExt) rm
8dc1d5d2552a181a17770eed0644f28438577dfacmaeder induced_from_to_morphism VSE rm s1 = fmap correctTarget
8dc1d5d2552a181a17770eed0644f28438577dfacmaeder . inducedFromToMorphismExt inducedExt (constMorphExt emptyMorExt)
8dc1d5d2552a181a17770eed0644f28438577dfacmaeder (\ _ _ -> return emptyMorExt) isSubProcsMap diffProcs rm s1
8dc1d5d2552a181a17770eed0644f28438577dfacmaederinstance Logic VSE ()
8dc1d5d2552a181a17770eed0644f28438577dfacmaeder VSEBasicSpec Sentence SYMB_ITEMS SYMB_MAP_ITEMS
8dc1d5d2552a181a17770eed0644f28438577dfacmaeder Symbol RawSymbol () where
876bd2c70a93981cc80f8376284616bce4a0fefcChristian Maeder stability VSE = Unstable
96a3f4b391a98d0e91bc1f608398442f29d4c69ecmaeder#ifdef UNI_PACKAGE
96a3f4b391a98d0e91bc1f608398442f29d4c69ecmaeder provers VSE = [vse]