Logic_CspCASL.hs revision f08f7774e4c47012f3c349205310750198cdc434
e9458b1a7a19a63aa4c179f9ab20f4d50681c168Jens ElknerModule : $Id$
1f0bfa2fbeea34f9ab8af45efcf50647c85c0ae5Ewaryst SchulzDescription : CspCASL instance of type class logic
1f0bfa2fbeea34f9ab8af45efcf50647c85c0ae5Ewaryst SchulzCopyright : (c) Markus Roggenbach, Till Mossakowski and Uni Bremen 2003
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
1f0bfa2fbeea34f9ab8af45efcf50647c85c0ae5Ewaryst SchulzMaintainer : M.Roggenbach@swansea.ac.uk
1f0bfa2fbeea34f9ab8af45efcf50647c85c0ae5Ewaryst SchulzStability : experimental
1f0bfa2fbeea34f9ab8af45efcf50647c85c0ae5Ewaryst SchulzPortability : non-portable(import Logic.Logic)
1f0bfa2fbeea34f9ab8af45efcf50647c85c0ae5Ewaryst SchulzHere is the place where the class Logic is instantiated for CspCASL.
1f0bfa2fbeea34f9ab8af45efcf50647c85c0ae5Ewaryst Schulz Also the instances for Syntax an Category.
de8eee2014437ec4020be15cd363257f87e79943Christian Maeder - writing real functions
1f0bfa2fbeea34f9ab8af45efcf50647c85c0ae5Ewaryst Schulz - Modul Sign.hs mit CSP-CASL-Signaturen und Morphismen, basiernd
1f0bfa2fbeea34f9ab8af45efcf50647c85c0ae5Ewaryst Schulz CSP-CASL-Signatur = (CASL-Sig,Menge von Kanalnamen)
9aec0bc9d57df2669c8095fb1b4bd954d80b5537Christian Maeder CSP-CASL-Morphismus = (CASL-Morphismus, Kanalnamenabbildung)
c7f1a9b3811f1ed427c57559d9af26a75a309ff1Ewaryst Schulz oder nur CASL-Morphismus
e24ccbc27ab90aa0bdb7064fd42e3bb0e0da6174Christian Maeder SYMB_ITEMS SYMB_MAP_ITEMS: erstmal von CASL (d.h. nur CASL-Morphismus)
1f7d5e06c0b9d99d257bdee9e8fb7bc000ec1d78Ewaryst Schulz - instance Sentences
c7f1a9b3811f1ed427c57559d9af26a75a309ff1Ewaryst Schulz S�tze = entweder CASL-S�tze oder CSP-CASL-S�tze
9aec0bc9d57df2669c8095fb1b4bd954d80b5537Christian Maeder Rest soweit wie m�glich von CASL �bernehmen
1f0bfa2fbeea34f9ab8af45efcf50647c85c0ae5Ewaryst Schulz - statische Analyse (gem�� Typ in Logic.Logic) schreiben
91b3147021cbeebb0590f4a577acba73142785c5Christian Maeder und unten f�r basic_analysis einh�ngen
1f0bfa2fbeea34f9ab8af45efcf50647c85c0ae5Ewaryst Schulz - Teillogiken (instance SemiLatticeWithTop ...)
1f0bfa2fbeea34f9ab8af45efcf50647c85c0ae5Ewaryst Schulzmodule CspCASL.Logic_CspCASL(CspCASL(CspCASL)) where
9aec0bc9d57df2669c8095fb1b4bd954d80b5537Christian Maederimport qualified Data.Set as Set
86c1b41a968fde92972d40753dbbd13e0b25d85bChristian Maederimport qualified CspCASL.AS_CspCASL as AS_CspCASL
86c1b41a968fde92972d40753dbbd13e0b25d85bChristian Maederimport qualified CspCASL.ATC_CspCASL()
86c1b41a968fde92972d40753dbbd13e0b25d85bChristian Maederimport qualified CspCASL.CspCASL_Keywords as CspCASL_Keywords
86c1b41a968fde92972d40753dbbd13e0b25d85bChristian Maederimport qualified CspCASL.Morphism as CspCASL_Morphism
de8eee2014437ec4020be15cd363257f87e79943Christian Maederimport qualified CspCASL.Parse_CspCASL as Parse_CspCASL
86c1b41a968fde92972d40753dbbd13e0b25d85bChristian Maederimport qualified CspCASL.Print_CspCASL ()
86c1b41a968fde92972d40753dbbd13e0b25d85bChristian Maederimport qualified CspCASL.SignCSP as SignCSP
86c1b41a968fde92972d40753dbbd13e0b25d85bChristian Maederimport qualified CspCASL.StatAnaCSP as StatAnaCSP
86c1b41a968fde92972d40753dbbd13e0b25d85bChristian Maeder-- | Lid for CspCASL
86c1b41a968fde92972d40753dbbd13e0b25d85bChristian Maederdata CspCASL = CspCASL deriving (Show)
e24ccbc27ab90aa0bdb7064fd42e3bb0e0da6174Christian Maederinstance Language CspCASL
9aec0bc9d57df2669c8095fb1b4bd954d80b5537Christian Maeder description _ =
e24ccbc27ab90aa0bdb7064fd42e3bb0e0da6174Christian Maeder "CspCASL - see\n\n"++
86c1b41a968fde92972d40753dbbd13e0b25d85bChristian Maeder "http://www.cs.swan.ac.uk/~csmarkus/ProcessesAndData/"
86c1b41a968fde92972d40753dbbd13e0b25d85bChristian Maederinstance SignExtension SignCSP.CspSign where
9aec0bc9d57df2669c8095fb1b4bd954d80b5537Christian Maeder isSubSignExtension = SignCSP.isInclusion
e49fd57c63845c7806860a9736ad09f6d44dbaedChristian Maeder-- | Instance for CspCASL morphism extension (used for Category)
3fea26a73b8fa69b22dfd2653d8f7bdacb45b9c9Christian Maederinstance MorphismExtension SignCSP.CspSign SignCSP.CspAddMorphism where
6c244f12ab0dc7ba1baf1413266093886a570e13Christian Maeder ideMorphismExtension _ = SignCSP.emptyCspAddMorphism
8a3ab31caff2bc2ad9355680186a7dd4da5f73b5Christian Maeder composeMorphismExtension = SignCSP.composeCspAddMorphism
9aec0bc9d57df2669c8095fb1b4bd954d80b5537Christian Maeder inverseMorphismExtension = SignCSP.inverseCspAddMorphism
86c1b41a968fde92972d40753dbbd13e0b25d85bChristian Maeder isInclusionMorphismExtension _ = True -- missing!
3fea26a73b8fa69b22dfd2653d8f7bdacb45b9c9Christian Maeder-- | Instance of Sentences for CspCASL (missing)
3fea26a73b8fa69b22dfd2653d8f7bdacb45b9c9Christian Maederinstance Sentences CspCASL
3fea26a73b8fa69b22dfd2653d8f7bdacb45b9c9Christian Maeder SignCSP.CspCASLSen -- sentence (missing)
3fea26a73b8fa69b22dfd2653d8f7bdacb45b9c9Christian Maeder Symbol -- symbol
86c1b41a968fde92972d40753dbbd13e0b25d85bChristian Maeder parse_sentence CspCASL = Nothing
86c1b41a968fde92972d40753dbbd13e0b25d85bChristian Maeder map_sen CspCASL mor sen =
9aec0bc9d57df2669c8095fb1b4bd954d80b5537Christian Maeder if isInclusionMorphism isInclusionMorphismExtension mor
9aec0bc9d57df2669c8095fb1b4bd954d80b5537Christian Maeder then return sen
86c1b41a968fde92972d40753dbbd13e0b25d85bChristian Maeder else fail "renaming in map_sen CspCASL not implemented"
86c1b41a968fde92972d40753dbbd13e0b25d85bChristian Maeder symmap_of CspCASL = morphismToSymbMap
86c1b41a968fde92972d40753dbbd13e0b25d85bChristian Maeder-- | Syntax of CspCASL
5b68f1141555736e0b7ddbe14218bcabcc44636fChristian Maederinstance Syntax CspCASL
86c1b41a968fde92972d40753dbbd13e0b25d85bChristian Maeder SYMB_ITEMS -- symb_items
86c1b41a968fde92972d40753dbbd13e0b25d85bChristian Maeder SYMB_MAP_ITEMS -- symb_map_items
9aec0bc9d57df2669c8095fb1b4bd954d80b5537Christian Maeder parse_basic_spec CspCASL =
86c1b41a968fde92972d40753dbbd13e0b25d85bChristian Maeder parse_symb_items CspCASL =
86c1b41a968fde92972d40753dbbd13e0b25d85bChristian Maeder Just $ symbItems CspCASL_Keywords.csp_casl_keywords
86c1b41a968fde92972d40753dbbd13e0b25d85bChristian Maeder parse_symb_map_items CspCASL =
dc62afbf79603699b39b2387f48298634f642e67cmaeder Just $ symbMapItems CspCASL_Keywords.csp_casl_keywords
86c1b41a968fde92972d40753dbbd13e0b25d85bChristian Maeder-- lattices (for sublogics) missing
86c1b41a968fde92972d40753dbbd13e0b25d85bChristian Maeder-- | Instance of Logic for CspCASL
9aec0bc9d57df2669c8095fb1b4bd954d80b5537Christian Maederinstance Logic CspCASL
9aec0bc9d57df2669c8095fb1b4bd954d80b5537Christian Maeder () -- Sublogics (missing)
86c1b41a968fde92972d40753dbbd13e0b25d85bChristian Maeder SignCSP.CspCASLSen -- sentence (missing)
5664bc775d5d61bbd5f71cf05f5c6dd5c63340ffChristian Maeder SYMB_ITEMS -- symb_items
9aec0bc9d57df2669c8095fb1b4bd954d80b5537Christian Maeder SYMB_MAP_ITEMS -- symb_map_items
9aec0bc9d57df2669c8095fb1b4bd954d80b5537Christian Maeder () -- proof_tree (missing)
86c1b41a968fde92972d40753dbbd13e0b25d85bChristian Maeder stability CspCASL = Experimental
9aec0bc9d57df2669c8095fb1b4bd954d80b5537Christian Maeder data_logic CspCASL = Just (Logic CASL)
3fea26a73b8fa69b22dfd2653d8f7bdacb45b9c9Christian Maeder empty_proof_tree _ = ()
e24ccbc27ab90aa0bdb7064fd42e3bb0e0da6174Christian Maeder-- | Static Analysis for CspCASL
3fea26a73b8fa69b22dfd2653d8f7bdacb45b9c9Christian Maederinstance StaticAnalysis CspCASL
9aec0bc9d57df2669c8095fb1b4bd954d80b5537Christian Maeder SignCSP.CspCASLSen -- sentence (missing)
9aec0bc9d57df2669c8095fb1b4bd954d80b5537Christian Maeder SYMB_ITEMS -- symb_items
9aec0bc9d57df2669c8095fb1b4bd954d80b5537Christian Maeder SYMB_MAP_ITEMS -- symb_map_items
9aec0bc9d57df2669c8095fb1b4bd954d80b5537Christian Maeder basic_analysis CspCASL =
9aec0bc9d57df2669c8095fb1b4bd954d80b5537Christian Maeder stat_symb_map_items CspCASL = error "Logic_CspCASL.hs"
9aec0bc9d57df2669c8095fb1b4bd954d80b5537Christian Maeder stat_symb_items CspCASL = error "Logic_CspCASL.hs"
9aec0bc9d57df2669c8095fb1b4bd954d80b5537Christian Maeder empty_signature CspCASL = SignCSP.emptyCspCASLSign
9aec0bc9d57df2669c8095fb1b4bd954d80b5537Christian Maeder inclusion CspCASL =
86c1b41a968fde92972d40753dbbd13e0b25d85bChristian Maeder SignCSP.isInclusion const -- this is still wrong
9aec0bc9d57df2669c8095fb1b4bd954d80b5537Christian Maeder signature_union CspCASL s =
86c1b41a968fde92972d40753dbbd13e0b25d85bChristian Maeder induced_from_morphism CspCASL = inducedFromMorphism
3be6a6e42bb49a1f99b0415fbc2e6330ab69e821Christian Maeder induced_from_to_morphism CspCASL = inducedFromToMorphism