hets/Comorphisms/CASL2CspCASL.hs

	CASL2CspCASL.hs revision b3dca469a9e267d6d71acfdeca7bf284d0581dc7
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder{- |
25cc5fbba63f84b47e389af749f55abbbde71c8cChristian MaederModule      :  $Header$
25cc5fbba63f84b47e389af749f55abbbde71c8cChristian MaederCopyright   :  (c) Till Mossakowski and Uni Bremen 2003
25cc5fbba63f84b47e389af749f55abbbde71c8cChristian MaederLicence     :  All rights reserved.
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederMaintainer  :  hets@tzi.de
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederStability   :  provisional
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederPortability :  non-portable (imports Logic.Logic)
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder   The embedding comorphism from CASL to CspCASL.
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder-}
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder
b9625461755578f3eed04676d42a63fd2caebd0cChristian Maedermodule Comorphisms.CASL2CspCASL where
b9625461755578f3eed04676d42a63fd2caebd0cChristian Maeder
88c66e48620750c42b94db9feb01b42ae23dba97Till Mossakowskiimport Logic.Logic
ac0bbbcb2774629bb87986e69cf53d3402c5f575Christian Maederimport Logic.Comorphism
760ae19a92dde8249679a674f93f58d26a7c5f6bChristian Maederimport Common.Id
760ae19a92dde8249679a674f93f58d26a7c5f6bChristian Maederimport Common.Lib.State
88c800932dd7053322501ea2039d9f234be6866cKlaus Luettichimport Common.AS_Annotation
8410667510a76409aca9bb24ff0eda0420088274Christian Maederimport qualified Common.Lib.Map as Map
8410667510a76409aca9bb24ff0eda0420088274Christian Maederimport qualified Common.Lib.Set as Set
8410667510a76409aca9bb24ff0eda0420088274Christian Maeder
404166b9366552e9ec5abb87a37c76ec8a815fb7Klaus Luettich-- CASL
404166b9366552e9ec5abb87a37c76ec8a815fb7Klaus Luettichimport CASL.Logic_CASL
fdb2d618144159395f7bf8ce3327b3c112a17dd3Till Mossakowskiimport CASL.Sublogic
404166b9366552e9ec5abb87a37c76ec8a815fb7Klaus Luettichimport CASL.Sign
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maederimport CASL.AS_Basic_CASL
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maederimport CASL.Morphism
d67a33b40578beef2e255a274f89bb9c34aaf056Christian Maeder
ac0bbbcb2774629bb87986e69cf53d3402c5f575Christian Maeder-- CspCASL
e593b89bfd4952698dc37feced21cefe869d87a2Christian Maederimport CspCASL.Logic_CspCASL
ac0bbbcb2774629bb87986e69cf53d3402c5f575Christian Maederimport CspCASL.AS_CSP_CASL
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maederimport CspCASL.SignCSP
760ae19a92dde8249679a674f93f58d26a7c5f6bChristian Maeder
760ae19a92dde8249679a674f93f58d26a7c5f6bChristian Maeder
c55a0f77be7e88d3620b419ec8961f4379a586e3Klaus Luettich-- | The identity of the comorphism
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maederdata CASL2CspCASL = CASL2CspCASL deriving (Show)
857992065be4ed40a72c6296b6c0aec62ab4c5b9Christian Maeder
857992065be4ed40a72c6296b6c0aec62ab4c5b9Christian Maederinstance Language CASL2CspCASL -- default definition is okay
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maederinstance Comorphism CASL2CspCASL
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder               CASL CASL_Sublogics
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder               CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder               CASLSign
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder               CASLMor
5d4038657f6a63e131f5804af2f7957b69e15a43Klaus Luettich               Symbol RawSymbol ()
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder               CspCASL ()
b0294d73dcefc502ddaa13e18b46103a5916971fTill Mossakowski               Basic_CSP_CASL_C_SPEC () SYMB_ITEMS SYMB_MAP_ITEMS
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder               CSPSign
77a65251ee036c6aaf09c2775315a4ee24259fbdJorina Freya Gerken               CSPMorphism
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder               () () () where
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder    sourceLogic CASL2CspCASL = CASL
4d7d7f9a423490731c73403c7806bd66967da946Christian Maeder    sourceSublogic CASL2CspCASL = CASL_SL
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder                      { has_sub = True, -- simple subsorting in CspCASL
97812b7ce9860bf514a8822a63503451795dbc65Klaus Luettich                        has_part = True,
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder                        has_cons = True,
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder                        has_eq = True,
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder                        has_pred = True,
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder                        which_logic = FOL
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder                      }
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder    targetLogic CASL2CspCASL = CspCASL
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder    targetSublogic CASL2CspCASL = ()
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder    map_sign CASL2CspCASL sig = let e = mapSig sig in Just (e, [])
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckers    map_morphism CASL2CspCASL = Just . mapMor
4e7050bcbcf0f372a5bad32ecd0282bccabf0983Klaus Luettich    --map_sentence CASL2CspCASL sig = Just . toSentence sig
ac0bbbcb2774629bb87986e69cf53d3402c5f575Christian Maeder    --map_symbol CASL2CspCASL = Set.single . mapSym
ac0bbbcb2774629bb87986e69cf53d3402c5f575Christian Maeder
33d042fe6a9eb27a4c48f840b80838f3e7d98e34Christian MaedermapSig :: CASLSign -> CSPSign
e593b89bfd4952698dc37feced21cefe869d87a2Christian MaedermapSig sign =
ac0bbbcb2774629bb87986e69cf53d3402c5f575Christian Maeder     (emptySign emptyCSPAddSign) {sortSet = sortSet sign
ce50fe187cdae64e75e510daafb78156280bdb91Christian Maeder           , sortRel = sortRel sign
ebe517300051f765f2ed856a789dd5613d681ab0Klaus Luettich               , opMap = opMap sign
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckers           , assocOps = assocOps sign
c55a0f77be7e88d3620b419ec8961f4379a586e3Klaus Luettich           , predMap = predMap sign }
6ae5607d2def114f998fd49bac4eef12a2620fafChristian Maeder
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaedermapMor :: CASLMor -> CSPMorphism
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaedermapMor m = Morphism {msource = mapSig $ msource m
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder               , mtarget = mapSig $ mtarget m
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder                   , sort_map = sort_map m
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder                   , fun_map = fun_map m
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder                   , pred_map = pred_map m
ebe517300051f765f2ed856a789dd5613d681ab0Klaus Luettich               , extended_map =
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckers                       CSPAddMorphism { channelMap = Map.empty,
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckers                                        processMap = Map.empty
c55a0f77be7e88d3620b419ec8961f4379a586e3Klaus Luettich                    }}
ac0bbbcb2774629bb87986e69cf53d3402c5f575Christian Maeder
ac0bbbcb2774629bb87986e69cf53d3402c5f575Christian Maeder