Hets - the Heterogeneous Tool Set

Copyright(c) Liam O'Reilly and Markus Roggenbach
Swansea University 2008
LicenseGPLv2 or higher, see LICENSE.txt
Maintainercsliam@swansea.ac.uk
Stabilityprovisional
Portabilityportable
Safe HaskellNone

CspCASLProver.TransProcesses

Description

Provides translations from Csp Processes to Isabelle terms

Synopsis

Documentation

transProcess :: CspCASLSign -> Sign () () -> Sign () () -> VSM -> PROCESS -> Term Source #

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 Source #

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.