{- |

Module : $Header$

Description : simplification of CspCASL sentences for output after analysis

Copyright : (c) Liam O'Reilly and Markus Roggenbach, Swansea University 2009

License : GPLv2 or higher, see LICENSE.txt

Maintainer : csliam@swansea.ac.uk

Stability : provisional

Portability : portable

Simplification of CspCASL sentences for output after analysis

-}

module CspCASL.SimplifySen (simplifySen) where

import CASL.AS_Basic_CASL (TERM (..), OP_SYMB (..))

import CASL.Sign (extendedInfo)

import CASL.SimplifySen (simplifyCASLSen, simplifyCASLTerm)

import Common.Id (simpleIdToId, nullRange)

import Common.Utils (isSingleton)

import qualified Common.Lib.MapSet as MapSet

import CspCASL.AS_CspCASL_Process

import CspCASL.SignCSP

{- | Simplify a CspCASL sentence for before pretty printing, e.g., for

"show theory". Typically this replaces fully quallified CASL by

non fully qualified CASL so that it is readable. -}

simplifySen :: CspCASLSign -> CspSen -> CspSen

simplifySen sigma sen =

case sen of

ProcessEq pn var alpha p ->

-- Simplify the process

let simpPn = simplifyFQProcName sigma pn

simpVar = simplifyFQProcVarList var

simpP = simplifyProc sigma p

in ProcessEq simpPn simpVar alpha simpP

-- | Simplifies a process name.

simplifyFQProcName :: CspCASLSign -> FQ_PROCESS_NAME -> FQ_PROCESS_NAME

simplifyFQProcName sig fqPn = let pn = procNameToSimpProcName fqPn in

if isSingleton $ MapSet.lookup pn $ procSet $ extendedInfo sig

then PROCESS_NAME pn else fqPn

-- | Simplifiy a fully qualified variable list

simplifyFQProcVarList :: FQProcVarList -> FQProcVarList

simplifyFQProcVarList fqvars =

{- Our fully qualified variable list is a list of CASL terms where each term

is a Qual_var. The CASL simplifier will refuse to simplify these as it

thinks you need the type as there is no application of a function or

predicate around the variable. Thus we do our own stripping. -}

let simplify (fqVar) = case fqVar of

Qual_var v _ _ -> Application (Op_name $ simpleIdToId v) [] nullRange

_ -> error

"CspCASL.SimplifySen.simplifyFQProcVarList: Unexpected CASL term"

in map simplify fqvars

{- | Simplifies the fully qualified CASL data and simplifies the fully

qualified processes down to non-fully qualified processes. -}

simplifyProc :: CspCASLSign -> PROCESS -> PROCESS

simplifyProc sigma proc =

let caslSign = ccSig2CASLSign sigma

in case proc of

Skip range ->

Skip range

Stop range ->

Stop range

Div range ->

Div range

Run es range ->

Run (simplifyEventSet es) range

Chaos es range ->

Chaos (simplifyEventSet es) range

PrefixProcess e p range ->

PrefixProcess (simplifyEvent sigma e) (simplifyProc sigma p) range

Sequential p q range ->

Sequential (simplifyProc sigma p) (simplifyProc sigma q) range

ExternalChoice p q range ->

ExternalChoice (simplifyProc sigma p) (simplifyProc sigma q) range

InternalChoice p q range ->

InternalChoice (simplifyProc sigma p) (simplifyProc sigma q) range

Interleaving p q range ->

Interleaving (simplifyProc sigma p) (simplifyProc sigma q) range

SynchronousParallel p q range ->

SynchronousParallel (simplifyProc sigma p)

(simplifyProc sigma q) range

GeneralisedParallel p es q range ->

GeneralisedParallel (simplifyProc sigma p)

(simplifyEventSet es)

(simplifyProc sigma q) range

AlphabetisedParallel p esp esq q range ->

AlphabetisedParallel (simplifyProc sigma p)

(simplifyEventSet esp)

(simplifyEventSet esq)

(simplifyProc sigma q) range

Hiding p es range ->

Hiding (simplifyProc sigma p) (simplifyEventSet es) range

RenamingProcess p r range ->

RenamingProcess (simplifyProc sigma p) r range

ConditionalProcess f p q range ->

ConditionalProcess (simplifyCASLSen caslSign f)

(simplifyProc sigma p)

(simplifyProc sigma q) range

NamedProcess name args range ->

let simpName = simplifyFQProcName sigma name

simpArgs = map (simplifyCASLTerm caslSign) args

in NamedProcess simpName simpArgs range

{- Throw away the FQProccess and just take the simplified inner

process. The inner processes range will be equal to this

processes range by construction. -}

FQProcess p _ _ ->

simplifyProc sigma p

{- | Simplifies the fully qualified events but using the casl

simplification of data and removed channel qualification. -}

simplifyEvent :: CspCASLSign -> EVENT -> EVENT

simplifyEvent sigma event =

let caslSign = ccSig2CASLSign sigma

simpCaslTerm = simplifyCASLTerm caslSign

in case event of

-- This is a non-fully qualified event anyway.

TermEvent t r -> TermEvent t r

-- This is a non-fully qualified event anyway.

ExternalPrefixChoice v s r -> ExternalPrefixChoice v s r

-- This is a non-fully qualified event anyway.

InternalPrefixChoice v s r -> InternalPrefixChoice v s r

-- This is a non-fully qualified event anyway.

ChanSend cn t r -> ChanSend cn t r

-- This is a non-fully qualified event anyway.

ChanNonDetSend cn v s r -> ChanNonDetSend cn v s r

-- This is a non-fully qualified event anyway.

ChanRecv cn v s r -> ChanRecv cn v s r

FQTermEvent t r -> TermEvent (simpCaslTerm t) r

FQExternalPrefixChoice fqVar r ->

let (v, s) = splitCASLVar fqVar

in ExternalPrefixChoice v s r

FQInternalPrefixChoice fqVar r ->

let (v, s) = splitCASLVar fqVar

in InternalPrefixChoice v s r

FQChanSend (cn, _) t r -> ChanSend cn (simpCaslTerm t) r

FQChanNonDetSend (cn, _) fqVar r ->

let (v, s) = splitCASLVar fqVar

in ChanNonDetSend cn v s r

FQChanRecv (cn, _) fqVar r ->

let (v, s) = splitCASLVar fqVar

in ChanRecv cn v s r

{- I am not really sure what to do with the sorts at the moment, can they be

compound sorts -- BUG? -}

{- | Simplifies the fully qualified event sets but using the casl

simplification of data and removed channel qualification. -}

simplifyEventSet :: EVENT_SET -> EVENT_SET

simplifyEventSet eventSet = eventSet