Trans_CspProver.hs revision 902bfaac7e88afebb6684fe1f2414ae2efbc7edf
f062ed7bd262a37a909dd77ce5fc23b446818823fieldingModule : $Id: Print_CspCASL.hs 9047 2007-10-13 15:24:00Z gimblett $
f062ed7bd262a37a909dd77ce5fc23b446818823fieldingDescription : Pretty printing for CspCASL
bc8fd1b0b1afdf89b8d28eefa8cd74e26ba97986fieldingCopyright : (c) Andy Gimblett, Liam O'Reilly and Markus Roggenbach, Swansea University 2008
f062ed7bd262a37a909dd77ce5fc23b446818823fieldingLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
2d2eda71267231c2526be701fe655db125852c1ffieldingMaintainer : csliam@swansea.ac.uk
2d2eda71267231c2526be701fe655db125852c1ffieldingStability : provisional
2d2eda71267231c2526be701fe655db125852c1ffieldingPortability : portable
2d2eda71267231c2526be701fe655db125852c1ffieldingtransforming Csp Processes to Isabelle terms
f062ed7bd262a37a909dd77ce5fc23b446818823fieldingtransProcess :: PROCESS -> Term
f062ed7bd262a37a909dd77ce5fc23b446818823fieldingtransProcess pr = case pr of
2d2eda71267231c2526be701fe655db125852c1ffielding -- precedence 0
f062ed7bd262a37a909dd77ce5fc23b446818823fielding Skip _ -> cspProver_skipOp
f062ed7bd262a37a909dd77ce5fc23b446818823fielding Stop _ -> cspProver_stopOp
f062ed7bd262a37a909dd77ce5fc23b446818823fielding Div _ -> cspProver_divOp
f062ed7bd262a37a909dd77ce5fc23b446818823fielding Run es _ -> App (cspProver_runOp) (transEventSet es) NotCont
2d2eda71267231c2526be701fe655db125852c1ffielding Chaos es _ -> App (cspProver_chaosOp) (transEventSet es) NotCont
f062ed7bd262a37a909dd77ce5fc23b446818823fielding NamedProcess pn ts _ ->
64185f9824e42f21ca7b9ae6c004484215c031a7rbb let pnTerm = conDouble $ show pn
2d2eda71267231c2526be701fe655db125852c1ffielding in if (null ts)
f062ed7bd262a37a909dd77ce5fc23b446818823fielding then pnTerm
f062ed7bd262a37a909dd77ce5fc23b446818823fielding else App pnTerm (conDouble $ show ts) NotCont
f062ed7bd262a37a909dd77ce5fc23b446818823fielding -- precedence 1
2d2eda71267231c2526be701fe655db125852c1ffielding ConditionalProcess f p q _ ->
f062ed7bd262a37a909dd77ce5fc23b446818823fielding ((keyword cspProver_ifS) <+> (pretty f) <+>
f062ed7bd262a37a909dd77ce5fc23b446818823fielding (keyword cspProver_thenS) <+> (glue pr p) <+>
f062ed7bd262a37a909dd77ce5fc23b446818823fielding (keyword cspProver_elseS) <+> (glue pr q)
f062ed7bd262a37a909dd77ce5fc23b446818823fielding -- precedence 2
f062ed7bd262a37a909dd77ce5fc23b446818823fielding Hiding p es _ ->
f062ed7bd262a37a909dd77ce5fc23b446818823fielding (pretty p) <+> (text cspProver_hidingS) <+> (pretty es)
2d2eda71267231c2526be701fe655db125852c1ffielding RenamingProcess p r _ ->
2d2eda71267231c2526be701fe655db125852c1ffielding ((pretty p) <+>
2d2eda71267231c2526be701fe655db125852c1ffielding (text cspProver_renaming_openS) <+>
f062ed7bd262a37a909dd77ce5fc23b446818823fielding (ppWithCommas r) <+>
f062ed7bd262a37a909dd77ce5fc23b446818823fielding (text cspProver_renaming_closeS))
2d2eda71267231c2526be701fe655db125852c1ffielding -- precedence 3
f062ed7bd262a37a909dd77ce5fc23b446818823fielding Sequential p q _ ->
f062ed7bd262a37a909dd77ce5fc23b446818823fielding cspProver_sequenceOp (transProcess p) (transProcess q)
f062ed7bd262a37a909dd77ce5fc23b446818823fielding-- (pretty p) <+> (text cspProver_sequenceS) <+> (glue pr q)
2d2eda71267231c2526be701fe655db125852c1ffielding{- PrefixProcess ev p _ ->
2d2eda71267231c2526be701fe655db125852c1ffielding (text "class(C_X") <+> (pretty ev) <> (text ")") <+> (text cspProver_prefixS) <+> (glue pr p)
2d2eda71267231c2526be701fe655db125852c1ffielding InternalPrefixProcess v s p _ ->
2d2eda71267231c2526be701fe655db125852c1ffielding ((text cspProver_internal_prefixS) <+> (pretty v) <+>
2d2eda71267231c2526be701fe655db125852c1ffielding (text cspProver_colonS) <+> (pretty s) <+>
fcc25eda7b150e226d3c1cdaea66a943d3fdee4erbb (text cspProver_prefixS) <+> (glue pr p)
ab5581cc78e9d865b0a6ab1404c53347b3276968rbb ExternalPrefixProcess v s p _ ->
92f3af936ce61f25358a3ee4f28df2f6d62040dfdreid ((text cspProver_external_prefixS) <+> (pretty v) <+>
fcc25eda7b150e226d3c1cdaea66a943d3fdee4erbb (text cspProver_colonS) <+> (pretty s) <+>
c9a95767fbf0f5fb0976a06b97a256033925e433rbb (text cspProver_prefixS) <+> (glue pr p)
2d2eda71267231c2526be701fe655db125852c1ffielding -- precedence 4
2d2eda71267231c2526be701fe655db125852c1ffielding InternalChoice p q _ ->
2d2eda71267231c2526be701fe655db125852c1ffielding (pretty p) <+> (text cspProver_internal_choiceS) <+> (glue pr q)
2d2eda71267231c2526be701fe655db125852c1ffielding ExternalChoice p q _ ->
61fd0cab072a05b855cbef9c585702401ac5ae29rbb (pretty p) <+> (text cspProver_external_choiceS) <+> (glue pr q)
61fd0cab072a05b855cbef9c585702401ac5ae29rbb -- precedence 5
61fd0cab072a05b855cbef9c585702401ac5ae29rbb Interleaving p q _ ->
61fd0cab072a05b855cbef9c585702401ac5ae29rbb (pretty p) <+> (text cspProver_interleavingS) <+> (glue pr q)
fd492f9543f14fb5bae78e04b135c3448eb9cc56rbb SynchronousParallel p q _ ->
fd492f9543f14fb5bae78e04b135c3448eb9cc56rbb (pretty p) <+> (text cspProver_synchronousS) <+> (glue pr q)
fd492f9543f14fb5bae78e04b135c3448eb9cc56rbb GeneralisedParallel p es q _ ->
fd492f9543f14fb5bae78e04b135c3448eb9cc56rbb cspProver_general_parallelOp (transProcess p) (transEventSet es) (transProcess q)
2d2eda71267231c2526be701fe655db125852c1ffielding AlphabetisedParallel p les res q _ ->
2d2eda71267231c2526be701fe655db125852c1ffielding cspProver_alphabetised_parallelOp (transProcess p) (transEventSet les) (transEventSet res) (transProcess q)
2d2eda71267231c2526be701fe655db125852c1ffielding-- glue and prec_comp decide whether the child in the parse tree needs
61fd0cab072a05b855cbef9c585702401ac5ae29rbb-- to be parenthesised or not. Parentheses are necessary if the
61fd0cab072a05b855cbef9c585702401ac5ae29rbb-- right-child is at the same level of precedence as the parent but is
61fd0cab072a05b855cbef9c585702401ac5ae29rbb-- a different operator; otherwise, they're not.
61fd0cab072a05b855cbef9c585702401ac5ae29rbbglue :: PROCESS -> PROCESS -> Doc
2d2eda71267231c2526be701fe655db125852c1ffieldingglue x y = if (prec_comp x y)
2d2eda71267231c2526be701fe655db125852c1ffielding then lparen <+> pretty y <+> rparen
bfb62a96023822c56c9120e4ee627d4091cc59c2rbb else pretty y
61fd0cab072a05b855cbef9c585702401ac5ae29rbb-- This is really nasty, but sledgehammer effective and allows fine
61fd0cab072a05b855cbef9c585702401ac5ae29rbb-- control. Unmaintainable, however. :-( I imagine there's a way to
61fd0cab072a05b855cbef9c585702401ac5ae29rbb-- compare the types in a less boilerplate manner, but OTOH there are
61fd0cab072a05b855cbef9c585702401ac5ae29rbb-- some special cases where it's nice to be explicit. Also, hiding
61fd0cab072a05b855cbef9c585702401ac5ae29rbb-- and renaming are distinctly non-standard. *shrug*
3d96ee83babeec32482c9082c9426340cee8c44dwroweprec_comp :: PROCESS -> PROCESS -> Bool
2d2eda71267231c2526be701fe655db125852c1ffieldingprec_comp x y =
61fd0cab072a05b855cbef9c585702401ac5ae29rbb Hiding _ _ _ ->
61fd0cab072a05b855cbef9c585702401ac5ae29rbb case y of RenamingProcess _ _ _ -> True
61fd0cab072a05b855cbef9c585702401ac5ae29rbb _ -> False
61fd0cab072a05b855cbef9c585702401ac5ae29rbb RenamingProcess _ _ _ ->
61fd0cab072a05b855cbef9c585702401ac5ae29rbb case y of Hiding _ _ _ -> True
61fd0cab072a05b855cbef9c585702401ac5ae29rbb _ -> False
61fd0cab072a05b855cbef9c585702401ac5ae29rbb Sequential _ _ _ ->
61fd0cab072a05b855cbef9c585702401ac5ae29rbb case y of InternalPrefixProcess _ _ _ _ -> True
2d2eda71267231c2526be701fe655db125852c1ffielding ExternalPrefixProcess _ _ _ _ -> True
2d2eda71267231c2526be701fe655db125852c1ffielding PrefixProcess _ _ _ ->
2d2eda71267231c2526be701fe655db125852c1ffielding case y of Sequential _ _ _ -> True
2d2eda71267231c2526be701fe655db125852c1ffielding InternalPrefixProcess _ _ _ _ ->
000b67449410515eac43e76ef6667915bfd4d2abgstein case y of Sequential _ _ _ -> True
2d2eda71267231c2526be701fe655db125852c1ffielding ExternalPrefixProcess _ _ _ _ ->
2d2eda71267231c2526be701fe655db125852c1ffielding case y of Sequential _ _ _ -> True
61fd0cab072a05b855cbef9c585702401ac5ae29rbb _ -> False
61fd0cab072a05b855cbef9c585702401ac5ae29rbb ExternalChoice _ _ _ ->
61fd0cab072a05b855cbef9c585702401ac5ae29rbb case y of InternalChoice _ _ _ -> True
61fd0cab072a05b855cbef9c585702401ac5ae29rbb _ -> False
7bdef86e15d47d16dcbe7a5611683191774bd5fbgstein InternalChoice _ _ _ ->
61fd0cab072a05b855cbef9c585702401ac5ae29rbb case y of ExternalChoice _ _ _ -> True
7bdef86e15d47d16dcbe7a5611683191774bd5fbgstein Interleaving _ _ _ ->
61fd0cab072a05b855cbef9c585702401ac5ae29rbb case y of SynchronousParallel _ _ _ -> True
61fd0cab072a05b855cbef9c585702401ac5ae29rbb GeneralisedParallel _ _ _ _ -> True
61fd0cab072a05b855cbef9c585702401ac5ae29rbb AlphabetisedParallel _ _ _ _ _ -> True
61fd0cab072a05b855cbef9c585702401ac5ae29rbb _ -> False
61fd0cab072a05b855cbef9c585702401ac5ae29rbb SynchronousParallel _ _ _ ->
61fd0cab072a05b855cbef9c585702401ac5ae29rbb case y of Interleaving _ _ _ -> True
3d96ee83babeec32482c9082c9426340cee8c44dwrowe GeneralisedParallel _ _ _ _ -> True
7bdef86e15d47d16dcbe7a5611683191774bd5fbgstein AlphabetisedParallel _ _ _ _ _ -> True
61fd0cab072a05b855cbef9c585702401ac5ae29rbb _ -> False
61fd0cab072a05b855cbef9c585702401ac5ae29rbb GeneralisedParallel _ _ _ _ ->
61fd0cab072a05b855cbef9c585702401ac5ae29rbb case y of Interleaving _ _ _ -> True
61fd0cab072a05b855cbef9c585702401ac5ae29rbb SynchronousParallel _ _ _ -> True
61fd0cab072a05b855cbef9c585702401ac5ae29rbb AlphabetisedParallel _ _ _ _ _ -> True
61fd0cab072a05b855cbef9c585702401ac5ae29rbb _ -> False
61fd0cab072a05b855cbef9c585702401ac5ae29rbb AlphabetisedParallel _ _ _ _ _ ->
61fd0cab072a05b855cbef9c585702401ac5ae29rbb case y of Interleaving _ _ _ -> True
3d96ee83babeec32482c9082c9426340cee8c44dwrowe SynchronousParallel _ _ _ -> True
7bdef86e15d47d16dcbe7a5611683191774bd5fbgstein GeneralisedParallel _ _ _ _ -> True
c9a95767fbf0f5fb0976a06b97a256033925e433rbb _ -> False
c9a95767fbf0f5fb0976a06b97a256033925e433rbb _ -> False
c9a95767fbf0f5fb0976a06b97a256033925e433rbbinstance Pretty EVENT where
c9a95767fbf0f5fb0976a06b97a256033925e433rbb pretty = printEvent
c9a95767fbf0f5fb0976a06b97a256033925e433rbbprintEvent :: EVENT -> Doc
c9a95767fbf0f5fb0976a06b97a256033925e433rbbprintEvent (TermEvent t _) = pretty t
c9a95767fbf0f5fb0976a06b97a256033925e433rbbprintEvent (ChanSend cn t _) = (pretty cn) <+>
c9a95767fbf0f5fb0976a06b97a256033925e433rbb (text chan_sendS) <+>
c9a95767fbf0f5fb0976a06b97a256033925e433rbb (pretty t)
c9a95767fbf0f5fb0976a06b97a256033925e433rbbprintEvent (ChanNonDetSend cn v s _) =
c9a95767fbf0f5fb0976a06b97a256033925e433rbb (pretty cn) <+> (text chan_sendS) <+>
61fd0cab072a05b855cbef9c585702401ac5ae29rbb (pretty v) <+> (text svar_sortS) <+> (pretty s)
61fd0cab072a05b855cbef9c585702401ac5ae29rbbprintEvent (ChanRecv cn v s _) =
61fd0cab072a05b855cbef9c585702401ac5ae29rbb (pretty cn) <+> (text chan_receiveS) <+>
61fd0cab072a05b855cbef9c585702401ac5ae29rbb (pretty v) <+> (text svar_sortS) <+> (pretty s)
61fd0cab072a05b855cbef9c585702401ac5ae29rbbinstance Pretty EVENT_SET where
61fd0cab072a05b855cbef9c585702401ac5ae29rbb pretty = printEventSet
3d96ee83babeec32482c9082c9426340cee8c44dwrowetransEventSet :: EVENT_SET -> Term
7bdef86e15d47d16dcbe7a5611683191774bd5fbgsteintransEventSet (EventSet _ _) = conDouble "not yet done"
61fd0cab072a05b855cbef9c585702401ac5ae29rbb--transEventSet (EventSet es _) = conDouble "not yet done"