Logic_CspCASL.hs revision 0a58641cb9f0c51d02626a826acde9785b4f4a36
1a38107941725211e7c3f051f7a8f5e12199f03acmaeder{-# LANGUAGE MultiParamTypeClasses, ScopedTypeVariables
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder , TypeSynonymInstances, FlexibleInstances #-}
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von SchroederDescription : CspCASL instance of type class logic
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuCopyright : (c) Markus Roggenbach, Till Mossakowski and Uni Bremen 2003
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von SchroederLicense : GPLv2 or higher, see LICENSE.txt
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von SchroederMaintainer : M.Roggenbach@swansea.ac.uk
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von SchroederStability : experimental
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von SchroederPortability : non-portable(import Logic.Logic)
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von SchroederHere is the place where the class Logic is instantiated for CspCASL. A
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von SchroederCspCASL signature is a CASL signature with a set of named channels and
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroederprocesses. Every process has a profile. Morphisms are supposed to allow
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroederrenaming of channels and processes, too. Also sublogics (as a superset of some
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von SchroederCASL sublogics) are still missing.
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder ( GenCspCASL (..)
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder , CspCASLSemantics
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder , failureCspCASL
1a38107941725211e7c3f051f7a8f5e12199f03acmaederimport qualified CASL.MapSentence as MapSen
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroederimport qualified CASL.SimplifySen as SimpSen
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroederimport CspCASL.Morphism as CspCASL_Morphism
1a38107941725211e7c3f051f7a8f5e12199f03acmaederimport qualified CspCASL.SignCSP as SignCSP
ba06b25b69be05a4733db7197940efd73976f215Jonathan von Schroederimport qualified CspCASL.SimplifySen as SimplifySen
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroederimport CspCASLProver.CspCASLProver (cspCASLProver)
1a38107941725211e7c3f051f7a8f5e12199f03acmaeder-- | a generic logic id for CspCASL with different semantics
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroederdata GenCspCASL a = GenCspCASL a deriving Show
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von SchroedercspCASL :: GenCspCASL ()
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von SchroedercspCASL = GenCspCASL ()
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder-- | The top-level logic with the loosest semantics (and without provers)
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroedertype CspCASL = GenCspCASL ()
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroederinstance Show a => Language (GenCspCASL a) where
656f17ae9b7610ff2de1b6eedeeadea0c3bcdc8dChristian Maeder language_name (GenCspCASL a) = "CspCASL"
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder ++ let s = show a in if s == "()" then "" else '_' : s
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder description _ =
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder "CspCASL - extension of CASL with the process algebra CSP\n" ++
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder "See http://www.cs.swan.ac.uk/~csmarkus/ProcessesAndData/"
ba06b25b69be05a4733db7197940efd73976f215Jonathan von Schroeder-- | Instance of Sentences for CspCASL
ba06b25b69be05a4733db7197940efd73976f215Jonathan von Schroederinstance Show a => Sentences (GenCspCASL a)
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder map_sen (GenCspCASL _) m = return . MapSen.mapSen mapSen m
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder sym_name (GenCspCASL _) = cspSymName
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder symmap_of (GenCspCASL _) = cspMorphismToCspSymbMap
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder simplify_sen (GenCspCASL _) =
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder SimpSen.simplifySen (const return) SimplifySen.simplifySen
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder sym_of (GenCspCASL _) = symSets
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder symKind (GenCspCASL _) = show . pretty . cspSymbType
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder print_named (GenCspCASL _) = printTheoryFormula
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder-- | Syntax of CspCASL
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroederinstance Show a => Syntax (GenCspCASL a)
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder CspBasicSpec -- basic_spec
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder CspSymbMapItems
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder parse_symb_items (GenCspCASL _) = Just cspSymbItems
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder parse_symb_map_items (GenCspCASL _) = Just cspSymbMapItems
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder parse_basic_spec (GenCspCASL _) = Just $ basicSpec startCspKeywords
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder-- lattices (for sublogics) missing
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroederclass Show a => CspCASLSemantics a where
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder cspProvers :: a
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder -> [Prover SignCSP.CspCASLSign SignCSP.CspCASLSen
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder CspCASL_Morphism.CspCASLMorphism () ()]
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder cspProvers _ = []
ba06b25b69be05a4733db7197940efd73976f215Jonathan von Schroeder{- further dummy types for the trace of the failure semantics can be added
ba06b25b69be05a4733db7197940efd73976f215Jonathan von Schroeder and made an instance of CspCASLSemantics.
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder "identity" Comorphisms between these different logics still need to be
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroederinstance CspCASLSemantics ()
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroederdata Trace = Trace deriving Show
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroederdata Failure = Failure deriving Show
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von SchroedertraceCspCASL :: GenCspCASL Trace
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von SchroedertraceCspCASL = GenCspCASL Trace
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von SchroederfailureCspCASL :: GenCspCASL Failure
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von SchroederfailureCspCASL = GenCspCASL Failure
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroederinstance CspCASLSemantics Trace where
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder cspProvers _ = [cspCASLProver]
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroederinstance CspCASLSemantics Failure
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder-- | Instance of Logic for CspCASL
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroederinstance CspCASLSemantics a => Logic (GenCspCASL a)
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder -- Sublogics (missing)
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder -- symb_map_items
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder CspSymbMapItems
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder -- proof_tree (missing)
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder stability (GenCspCASL _) = Testing
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder data_logic (GenCspCASL _) = Just (Logic CASL)
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder empty_proof_tree _ = ()
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder provers (GenCspCASL _) = cspProvers (undefined :: a)
empty_signature (GenCspCASL _) = SignCSP.emptyCspCASLSign
is_subsig (GenCspCASL _) = SignCSP.isCspCASLSubSig
signature_union (GenCspCASL _) = SignCSP.unionCspCASLSign
signatureDiff (GenCspCASL _) s = return . diffSig SignCSP.diffCspSig s
morphismUnion CspCASL_Morphism.cspAddMorphismUnion