Trans_CspProver.hs revision c82d338435cec74cc01b5af5b8648defc81a2e53
7a8401ce858002b67e8f4198fde45a1562696ccbChristian Maeder{- |
50dce6b011347f92377adb8bbabaeeb80975e86dChristian MaederModule : $Header$
e374cd77f3dbe95289afa9431d36a8a8a8fdc81fChristian MaederDescription : Provides transformations from Csp Processes to Isabelle terms
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederCopyright : (c) Andy Gimblett, Liam O'Reilly and Markus Roggenbach,
50dce6b011347f92377adb8bbabaeeb80975e86dChristian Maeder Swansea University 2008
34bff097c14521b5e57ce37279a34256e1f78aa5Klaus LuettichLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
50dce6b011347f92377adb8bbabaeeb80975e86dChristian Maeder
50dce6b011347f92377adb8bbabaeeb80975e86dChristian MaederMaintainer : csliam@swansea.ac.uk
50dce6b011347f92377adb8bbabaeeb80975e86dChristian MaederStability : provisional
f3a94a197960e548ecd6520bb768cb0d547457bbChristian MaederPortability : portable
c2db39a683438b0f3d484519f4c93db26eec9d2eWiebke Herding
c2db39a683438b0f3d484519f4c93db26eec9d2eWiebke HerdingProvides transformations from Csp Processes to Isabelle terms
c2db39a683438b0f3d484519f4c93db26eec9d2eWiebke Herding
c2db39a683438b0f3d484519f4c93db26eec9d2eWiebke Herding-}
50dce6b011347f92377adb8bbabaeeb80975e86dChristian Maedermodule CspCASL.Trans_CspProver where
50dce6b011347f92377adb8bbabaeeb80975e86dChristian Maeder
ad270004874ce1d0697fb30d7309f180553bb315Christian Maederimport qualified CASL.AS_Basic_CASL as CASL_AS_Basic_CASL
2bb4c0b7bc54ce51e68bff86b3a19be16e0f0449Christian Maederimport CASL.Fold as CASL_Fold
1a11b3b997a32ebf7d52758dea143ef361fd9d5bChristian Maederimport qualified CASL.Sign as CASL_Sign
40f1a7ea3e3ed12cbeca205918b645dabed0402aChristian Maeder
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maederimport Common.Id
50dce6b011347f92377adb8bbabaeeb80975e86dChristian Maeder
50dce6b011347f92377adb8bbabaeeb80975e86dChristian Maederimport qualified Comorphisms.CFOL2IsabelleHOL as CFOL2IsabelleHOL
bfa3df9a76eebd7d6934623e99194ad954be54eaKlaus Luettich
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wangimport CspCASL.AS_CspCASL_Process
50dce6b011347f92377adb8bbabaeeb80975e86dChristian Maederimport CspCASL.CspProver_Consts
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wangimport CspCASL.Trans_Consts
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang
e374cd77f3dbe95289afa9431d36a8a8a8fdc81fChristian Maederimport Isabelle.IsaSign
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wangimport Isabelle.IsaConsts
e374cd77f3dbe95289afa9431d36a8a8a8fdc81fChristian Maeder
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun WangtransProcess :: CASL_Sign.Sign () () -> PROCESS -> Term
e374cd77f3dbe95289afa9431d36a8a8a8fdc81fChristian MaedertransProcess caslSign pr = case pr of
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang -- precedence 0
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang Skip _ -> cspProver_skipOp
c64f180c7a3053a773d91a00226073d565fab46bChristian Maeder Stop _ -> cspProver_stopOp
1a11b3b997a32ebf7d52758dea143ef361fd9d5bChristian Maeder Div _ -> cspProver_divOp
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang Run es _ -> App (cspProver_runOp) (transEventSet es) NotCont
c64f180c7a3053a773d91a00226073d565fab46bChristian Maeder Chaos es _ -> App (cspProver_chaosOp) (transEventSet es) NotCont
1a11b3b997a32ebf7d52758dea143ef361fd9d5bChristian Maeder NamedProcess pn ts _ ->
50dce6b011347f92377adb8bbabaeeb80975e86dChristian Maeder let pnTerm = conDouble $ show pn
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang in if (null ts)
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang then pnTerm
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang else App pnTerm (conDouble $ show ts) NotCont
50dce6b011347f92377adb8bbabaeeb80975e86dChristian Maeder -- precedence 1
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang ConditionalProcess _ p q _ ->
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang cspProver_conditionalOp true (transProcess caslSign p)
1a11b3b997a32ebf7d52758dea143ef361fd9d5bChristian Maeder (transProcess caslSign q)
1a11b3b997a32ebf7d52758dea143ef361fd9d5bChristian Maeder -- precedence 2
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang Hiding p es _ ->
1a11b3b997a32ebf7d52758dea143ef361fd9d5bChristian Maeder cspProver_hidingOp (transProcess caslSign p) (transEventSet es)
1a11b3b997a32ebf7d52758dea143ef361fd9d5bChristian Maeder RenamingProcess p r _ ->
50dce6b011347f92377adb8bbabaeeb80975e86dChristian Maeder cspProver_renamingOp (transProcess caslSign p) (transRenaming r)
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang -- precedence 3
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang Sequential p q _ ->
e374cd77f3dbe95289afa9431d36a8a8a8fdc81fChristian Maeder cspProver_sequenceOp (transProcess caslSign p) (transProcess caslSign q)
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder -- BUG - this is not right yet
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder PrefixProcess ev p _ ->
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang cspProver_action_prefixOp (transEvent caslSign ev)
1a11b3b997a32ebf7d52758dea143ef361fd9d5bChristian Maeder (transProcess caslSign p)
1a11b3b997a32ebf7d52758dea143ef361fd9d5bChristian Maeder -- precedence 4
1a11b3b997a32ebf7d52758dea143ef361fd9d5bChristian Maeder InternalChoice p q _ ->
50dce6b011347f92377adb8bbabaeeb80975e86dChristian Maeder cspProver_internal_choiceOp (transProcess caslSign p)
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang (transProcess caslSign q)
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang ExternalChoice p q _ ->
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder cspProver_external_choiceOp (transProcess caslSign p)
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang (transProcess caslSign q)
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang -- precedence 5
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang Interleaving p q _ ->
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang cspProver_interleavingOp (transProcess caslSign p)
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang (transProcess caslSign q)
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang SynchronousParallel p q _ ->
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang cspProver_synchronousOp (transProcess caslSign p)
1a11b3b997a32ebf7d52758dea143ef361fd9d5bChristian Maeder (transProcess caslSign q)
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang GeneralisedParallel p es q _ ->
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang cspProver_general_parallelOp (transProcess caslSign p)
1a11b3b997a32ebf7d52758dea143ef361fd9d5bChristian Maeder (transEventSet es)
1a11b3b997a32ebf7d52758dea143ef361fd9d5bChristian Maeder (transProcess caslSign q)
c64f180c7a3053a773d91a00226073d565fab46bChristian Maeder
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang AlphabetisedParallel p les res q _ ->
1a11b3b997a32ebf7d52758dea143ef361fd9d5bChristian Maeder cspProver_alphabetised_parallelOp (transProcess caslSign p)
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang (transEventSet les)
c64f180c7a3053a773d91a00226073d565fab46bChristian Maeder (transEventSet res)
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang (transProcess caslSign q)
c64f180c7a3053a773d91a00226073d565fab46bChristian Maeder -- BUG not done right yet
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang FQProcess p _ _ ->
c64f180c7a3053a773d91a00226073d565fab46bChristian Maeder transProcess caslSign p
1a11b3b997a32ebf7d52758dea143ef361fd9d5bChristian Maeder
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun WangtransEventSet :: EVENT_SET -> Term
e374cd77f3dbe95289afa9431d36a8a8a8fdc81fChristian MaedertransEventSet evs =
e374cd77f3dbe95289afa9431d36a8a8a8fdc81fChristian Maeder let
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder -- tran_COMM_TYPE ct = conDouble $ (tokStr ct) ++ barExtS
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder -- tran_commType ct = conDouble $ (tokStr ct) ++ barExtS
bfa3df9a76eebd7d6934623e99194ad954be54eaKlaus Luettich in case evs of
bfa3df9a76eebd7d6934623e99194ad954be54eaKlaus Luettich EventSet _ _ -> conDouble "ChanSendNotYetDone"
bfa3df9a76eebd7d6934623e99194ad954be54eaKlaus Luettich -- Set $ FixedSet $ map tran_COMM_TYPE commTypes
bfa3df9a76eebd7d6934623e99194ad954be54eaKlaus Luettich FQEventSet _ _ -> conDouble "ChanSendNotYetDone"
bfa3df9a76eebd7d6934623e99194ad954be54eaKlaus Luettich -- Set $ FixedSet $ map tranCommType commTypes
bfa3df9a76eebd7d6934623e99194ad954be54eaKlaus Luettich
bfa3df9a76eebd7d6934623e99194ad954be54eaKlaus Luettich-- BUG - this is not right yet
e374cd77f3dbe95289afa9431d36a8a8a8fdc81fChristian MaedertransEvent :: CASL_Sign.Sign () () -> EVENT -> Term
bfa3df9a76eebd7d6934623e99194ad954be54eaKlaus LuettichtransEvent caslSign ev =
bfa3df9a76eebd7d6934623e99194ad954be54eaKlaus Luettich case ev of
1a11b3b997a32ebf7d52758dea143ef361fd9d5bChristian Maeder TermEvent caslTerm _ -> transTerm_with_class caslSign caslTerm
bfa3df9a76eebd7d6934623e99194ad954be54eaKlaus Luettich InternalPrefixChoice _ _ _ ->
e374cd77f3dbe95289afa9431d36a8a8a8fdc81fChristian Maeder conDouble "ChanSendNotYetDone"
-- cspProver_internal_prefix_choiceOp (transVar v) (transSort s)
ExternalPrefixChoice _ _ _ ->
conDouble "ChanSendNotYetDone"
-- cspProver_external_prefix_choiceOp (transVar v) (transSort s)
ChanSend _ _ _ -> conDouble "ChanSendNotYetDone"
ChanNonDetSend _ _ _ _ -> conDouble "ChanNonDetSendNotYetDone"
ChanRecv _ _ _ _ -> conDouble "ChanRecvNotYetDone"
-- BUG - this is not done at all
FQEvent _ _ fqTerm r -> transEvent caslSign (TermEvent fqTerm r)
transVar :: CASL_AS_Basic_CASL.VAR -> Term
transVar v = conDouble $ tokStr v
transSort :: CASL_AS_Basic_CASL.SORT -> Term
transSort sort = let sortBarString = convertSort2String sort ++ barExtS
in conDouble sortBarString
transRenaming :: RENAMING -> Term
transRenaming _ = conDouble "not yet done"
transTerm_with_class :: CASL_Sign.Sign () () -> CASL_AS_Basic_CASL.TERM () ->
Term
transTerm_with_class caslSign caslTerm =
let strs = CFOL2IsabelleHOL.getAssumpsToks caslSign in
case caslTerm of
-- if the term is just a variable then we just translate the
-- variable to isabelle
CASL_AS_Basic_CASL.Qual_var v _ _ ->
mkFree $ CFOL2IsabelleHOL.transVar strs v
-- otherwise we add a classOp around it and translate the inside of
-- it with the translator that adds a chooseOp
_ -> classOp (transCaslTerm caslSign caslTerm)
-- | Translate a CASL Term to an Isabelle Term using the exact
-- translation as is done in the comorphism composition
-- CASL2PCFOL;defaultCASL2SubCFOL;CFOL2IsabelleHOL
transCaslTerm :: CASL_Sign.Sign () () -> CASL_AS_Basic_CASL.TERM () -> Term
transCaslTerm caslSign caslTerm =
let tyToks = CFOL2IsabelleHOL.typeToks caslSign
trForm = CFOL2IsabelleHOL.formTrCASL
strs = CFOL2IsabelleHOL.getAssumpsToks caslSign
in CASL_Fold.foldTerm (CFOL2IsabelleHOL.transRecord
caslSign tyToks trForm strs)
{ foldQual_var = \ _ v s _ -> termAppl (conDouble $ "choose_" ++ show s)
$ mkFree $ CFOL2IsabelleHOL.transVar strs v }
caslTerm