| Copyright | (c) Liam O'Reilly and Markus Roggenbach, Swansea University 2008 |
|---|---|
| License | GPLv2 or higher, see LICENSE.txt |
| Maintainer | csliam@swansea.ac.uk |
| Stability | provisional |
| Portability | portable |
| Safe Haskell | None |
CspCASLProver.TransProcesses
Description
Provides translations from Csp Processes to Isabelle terms
- transProcess :: CspCASLSign -> Sign () () -> Sign () () -> VSM -> PROCESS -> Term
- data VarSource
Documentation
transProcess :: CspCASLSign -> Sign () () -> Sign () () -> VSM -> PROCESS -> Term
Translate a Process into CspProver (Isabelle). We need the data part (CASL signature) for translating the translation of terms. We also need the global variables so we can treat local and global variables different. We need the PCFOL and CFOL signature of the data part after translation to PCFOL and CFOL to pass along to the term and formula translations.
data VarSource
The origin of a variable
Constructors
| PrefixChoice | indicates that the variable originated from a prefix choice operator. |
| ChanSendOrRec SORT | indicates that the variable originated from a channel nondeterministic send or channel receive where the sort is the declared sort of the channel. |
| GlobalParameter | indicates that the variable originated from global parameter to the process. |