{- |
Module      :  ./CspCASL/SimplifySen.hs
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 :: CspCASLSign -> CspSen -> CspSen
simplifySen sigma :: CspCASLSign
sigma sen :: CspSen
sen =
    case CspSen
sen of
      ProcessEq pn :: FQ_PROCESS_NAME
pn var :: FQProcVarList
var alpha :: CommAlpha
alpha p :: PROCESS
p ->
          -- Simplify the process
          let simpPn :: FQ_PROCESS_NAME
simpPn = CspCASLSign -> FQ_PROCESS_NAME -> FQ_PROCESS_NAME
simplifyFQProcName CspCASLSign
sigma FQ_PROCESS_NAME
pn
              simpVar :: FQProcVarList
simpVar = FQProcVarList -> FQProcVarList
simplifyFQProcVarList FQProcVarList
var
              simpP :: PROCESS
simpP = CspCASLSign -> PROCESS -> PROCESS
simplifyProc CspCASLSign
sigma PROCESS
p
          in FQ_PROCESS_NAME -> FQProcVarList -> CommAlpha -> PROCESS -> CspSen
ProcessEq FQ_PROCESS_NAME
simpPn FQProcVarList
simpVar CommAlpha
alpha PROCESS
simpP

-- | Simplifies a process name.
simplifyFQProcName :: CspCASLSign -> FQ_PROCESS_NAME -> FQ_PROCESS_NAME
simplifyFQProcName :: CspCASLSign -> FQ_PROCESS_NAME -> FQ_PROCESS_NAME
simplifyFQProcName sig :: CspCASLSign
sig fqPn :: FQ_PROCESS_NAME
fqPn = let pn :: PROCESS_NAME
pn = FQ_PROCESS_NAME -> PROCESS_NAME
procNameToSimpProcName FQ_PROCESS_NAME
fqPn in
  if Set ProcProfile -> Bool
forall a. Set a -> Bool
isSingleton (Set ProcProfile -> Bool) -> Set ProcProfile -> Bool
forall a b. (a -> b) -> a -> b
$ PROCESS_NAME -> MapSet PROCESS_NAME ProcProfile -> Set ProcProfile
forall a b. Ord a => a -> MapSet a b -> Set b
MapSet.lookup PROCESS_NAME
pn (MapSet PROCESS_NAME ProcProfile -> Set ProcProfile)
-> MapSet PROCESS_NAME ProcProfile -> Set ProcProfile
forall a b. (a -> b) -> a -> b
$ CspSign -> MapSet PROCESS_NAME ProcProfile
procSet (CspSign -> MapSet PROCESS_NAME ProcProfile)
-> CspSign -> MapSet PROCESS_NAME ProcProfile
forall a b. (a -> b) -> a -> b
$ CspCASLSign -> CspSign
forall f e. Sign f e -> e
extendedInfo CspCASLSign
sig
  then PROCESS_NAME -> FQ_PROCESS_NAME
PROCESS_NAME PROCESS_NAME
pn else FQ_PROCESS_NAME
fqPn

-- | Simplifiy a fully qualified variable list
simplifyFQProcVarList :: FQProcVarList -> FQProcVarList
simplifyFQProcVarList :: FQProcVarList -> FQProcVarList
simplifyFQProcVarList fqvars :: FQProcVarList
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 :: TERM f -> TERM f
simplify (TERM f
fqVar) = case TERM f
fqVar of
        Qual_var v :: VAR
v _ _ -> OP_SYMB -> [TERM f] -> Range -> TERM f
forall f. OP_SYMB -> [TERM f] -> Range -> TERM f
Application (PROCESS_NAME -> OP_SYMB
Op_name (PROCESS_NAME -> OP_SYMB) -> PROCESS_NAME -> OP_SYMB
forall a b. (a -> b) -> a -> b
$ VAR -> PROCESS_NAME
simpleIdToId VAR
v) [] Range
nullRange
        _ -> [Char] -> TERM f
forall a. HasCallStack => [Char] -> a
error
          "CspCASL.SimplifySen.simplifyFQProcVarList: Unexpected CASL term"
    in (TERM () -> TERM ()) -> FQProcVarList -> FQProcVarList
forall a b. (a -> b) -> [a] -> [b]
map TERM () -> TERM ()
forall f f. TERM f -> TERM f
simplify FQProcVarList
fqvars

{- | Simplifies the fully qualified CASL data and simplifies the fully
qualified processes down to non-fully qualified processes. -}
simplifyProc :: CspCASLSign -> PROCESS -> PROCESS
simplifyProc :: CspCASLSign -> PROCESS -> PROCESS
simplifyProc sigma :: CspCASLSign
sigma proc :: PROCESS
proc =
    let caslSign :: CASLSign
caslSign = CspCASLSign -> CASLSign
ccSig2CASLSign CspCASLSign
sigma
    in case PROCESS
proc of
      Skip range :: Range
range ->
          Range -> PROCESS
Skip Range
range
      Stop range :: Range
range ->
          Range -> PROCESS
Stop Range
range
      Div range :: Range
range ->
          Range -> PROCESS
Div Range
range
      Run es :: EVENT_SET
es range :: Range
range ->
          EVENT_SET -> Range -> PROCESS
Run (EVENT_SET -> EVENT_SET
simplifyEventSet EVENT_SET
es) Range
range
      Chaos es :: EVENT_SET
es range :: Range
range ->
          EVENT_SET -> Range -> PROCESS
Chaos (EVENT_SET -> EVENT_SET
simplifyEventSet EVENT_SET
es) Range
range
      PrefixProcess e :: EVENT
e p :: PROCESS
p range :: Range
range ->
          EVENT -> PROCESS -> Range -> PROCESS
PrefixProcess (CspCASLSign -> EVENT -> EVENT
simplifyEvent CspCASLSign
sigma EVENT
e) (CspCASLSign -> PROCESS -> PROCESS
simplifyProc CspCASLSign
sigma PROCESS
p) Range
range
      Sequential p :: PROCESS
p q :: PROCESS
q range :: Range
range ->
          PROCESS -> PROCESS -> Range -> PROCESS
Sequential (CspCASLSign -> PROCESS -> PROCESS
simplifyProc CspCASLSign
sigma PROCESS
p) (CspCASLSign -> PROCESS -> PROCESS
simplifyProc CspCASLSign
sigma PROCESS
q) Range
range
      ExternalChoice p :: PROCESS
p q :: PROCESS
q range :: Range
range ->
          PROCESS -> PROCESS -> Range -> PROCESS
ExternalChoice (CspCASLSign -> PROCESS -> PROCESS
simplifyProc CspCASLSign
sigma PROCESS
p) (CspCASLSign -> PROCESS -> PROCESS
simplifyProc CspCASLSign
sigma PROCESS
q) Range
range
      InternalChoice p :: PROCESS
p q :: PROCESS
q range :: Range
range ->
          PROCESS -> PROCESS -> Range -> PROCESS
InternalChoice (CspCASLSign -> PROCESS -> PROCESS
simplifyProc CspCASLSign
sigma PROCESS
p) (CspCASLSign -> PROCESS -> PROCESS
simplifyProc CspCASLSign
sigma PROCESS
q) Range
range
      Interleaving p :: PROCESS
p q :: PROCESS
q range :: Range
range ->
          PROCESS -> PROCESS -> Range -> PROCESS
Interleaving (CspCASLSign -> PROCESS -> PROCESS
simplifyProc CspCASLSign
sigma PROCESS
p) (CspCASLSign -> PROCESS -> PROCESS
simplifyProc CspCASLSign
sigma PROCESS
q) Range
range
      SynchronousParallel p :: PROCESS
p q :: PROCESS
q range :: Range
range ->
          PROCESS -> PROCESS -> Range -> PROCESS
SynchronousParallel (CspCASLSign -> PROCESS -> PROCESS
simplifyProc CspCASLSign
sigma PROCESS
p)
                                  (CspCASLSign -> PROCESS -> PROCESS
simplifyProc CspCASLSign
sigma PROCESS
q) Range
range
      GeneralisedParallel p :: PROCESS
p es :: EVENT_SET
es q :: PROCESS
q range :: Range
range ->
          PROCESS -> EVENT_SET -> PROCESS -> Range -> PROCESS
GeneralisedParallel (CspCASLSign -> PROCESS -> PROCESS
simplifyProc CspCASLSign
sigma PROCESS
p)
                                  (EVENT_SET -> EVENT_SET
simplifyEventSet EVENT_SET
es)
                                  (CspCASLSign -> PROCESS -> PROCESS
simplifyProc CspCASLSign
sigma PROCESS
q) Range
range
      AlphabetisedParallel p :: PROCESS
p esp :: EVENT_SET
esp esq :: EVENT_SET
esq q :: PROCESS
q range :: Range
range ->
          PROCESS -> EVENT_SET -> EVENT_SET -> PROCESS -> Range -> PROCESS
AlphabetisedParallel (CspCASLSign -> PROCESS -> PROCESS
simplifyProc CspCASLSign
sigma PROCESS
p)
                                   (EVENT_SET -> EVENT_SET
simplifyEventSet EVENT_SET
esp)
                                   (EVENT_SET -> EVENT_SET
simplifyEventSet EVENT_SET
esq)
                                   (CspCASLSign -> PROCESS -> PROCESS
simplifyProc CspCASLSign
sigma PROCESS
q) Range
range
      Hiding p :: PROCESS
p es :: EVENT_SET
es range :: Range
range ->
          PROCESS -> EVENT_SET -> Range -> PROCESS
Hiding (CspCASLSign -> PROCESS -> PROCESS
simplifyProc CspCASLSign
sigma PROCESS
p) (EVENT_SET -> EVENT_SET
simplifyEventSet EVENT_SET
es) Range
range
      RenamingProcess p :: PROCESS
p r :: RENAMING
r range :: Range
range ->
          PROCESS -> RENAMING -> Range -> PROCESS
RenamingProcess (CspCASLSign -> PROCESS -> PROCESS
simplifyProc CspCASLSign
sigma PROCESS
p) RENAMING
r Range
range
      ConditionalProcess f :: FORMULA ()
f p :: PROCESS
p q :: PROCESS
q range :: Range
range ->
          FORMULA () -> PROCESS -> PROCESS -> Range -> PROCESS
ConditionalProcess (CASLSign -> FORMULA () -> FORMULA ()
forall f e.
(FormExtension f, TermExtension f) =>
Sign f e -> FORMULA f -> FORMULA f
simplifyCASLSen CASLSign
caslSign FORMULA ()
f)
                                 (CspCASLSign -> PROCESS -> PROCESS
simplifyProc CspCASLSign
sigma PROCESS
p)
                                 (CspCASLSign -> PROCESS -> PROCESS
simplifyProc CspCASLSign
sigma PROCESS
q) Range
range
      NamedProcess name :: FQ_PROCESS_NAME
name args :: FQProcVarList
args range :: Range
range ->
        let simpName :: FQ_PROCESS_NAME
simpName = CspCASLSign -> FQ_PROCESS_NAME -> FQ_PROCESS_NAME
simplifyFQProcName CspCASLSign
sigma FQ_PROCESS_NAME
name
            simpArgs :: FQProcVarList
simpArgs = (TERM () -> TERM ()) -> FQProcVarList -> FQProcVarList
forall a b. (a -> b) -> [a] -> [b]
map (CASLSign -> TERM () -> TERM ()
forall f e.
(FormExtension f, TermExtension f) =>
Sign f e -> TERM f -> TERM f
simplifyCASLTerm CASLSign
caslSign) FQProcVarList
args
        in FQ_PROCESS_NAME -> FQProcVarList -> Range -> PROCESS
NamedProcess FQ_PROCESS_NAME
simpName FQProcVarList
simpArgs Range
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 :: PROCESS
p _ _ ->
          CspCASLSign -> PROCESS -> PROCESS
simplifyProc CspCASLSign
sigma PROCESS
p

{- | Simplifies the fully qualified events but using the casl
simplification of data and removed channel qualification. -}
simplifyEvent :: CspCASLSign -> EVENT -> EVENT
simplifyEvent :: CspCASLSign -> EVENT -> EVENT
simplifyEvent sigma :: CspCASLSign
sigma event :: EVENT
event =
  let caslSign :: CASLSign
caslSign = CspCASLSign -> CASLSign
ccSig2CASLSign CspCASLSign
sigma
      simpCaslTerm :: TERM () -> TERM ()
simpCaslTerm = CASLSign -> TERM () -> TERM ()
forall f e.
(FormExtension f, TermExtension f) =>
Sign f e -> TERM f -> TERM f
simplifyCASLTerm CASLSign
caslSign
  in case EVENT
event of
      -- This is a non-fully qualified event anyway.
      TermEvent t :: TERM ()
t r :: Range
r -> TERM () -> Range -> EVENT
TermEvent TERM ()
t Range
r
      -- This is a non-fully qualified event anyway.
      ExternalPrefixChoice v :: VAR
v s :: PROCESS_NAME
s r :: Range
r -> VAR -> PROCESS_NAME -> Range -> EVENT
ExternalPrefixChoice VAR
v PROCESS_NAME
s Range
r
      -- This is a non-fully qualified event anyway.
      InternalPrefixChoice v :: VAR
v s :: PROCESS_NAME
s r :: Range
r -> VAR -> PROCESS_NAME -> Range -> EVENT
InternalPrefixChoice VAR
v PROCESS_NAME
s Range
r
      -- This is a non-fully qualified event anyway.
      ChanSend cn :: PROCESS_NAME
cn t :: TERM ()
t r :: Range
r -> PROCESS_NAME -> TERM () -> Range -> EVENT
ChanSend PROCESS_NAME
cn TERM ()
t Range
r
      -- This is a non-fully qualified event anyway.
      ChanNonDetSend cn :: PROCESS_NAME
cn v :: VAR
v s :: PROCESS_NAME
s r :: Range
r -> PROCESS_NAME -> VAR -> PROCESS_NAME -> Range -> EVENT
ChanNonDetSend PROCESS_NAME
cn VAR
v PROCESS_NAME
s Range
r
      -- This is a non-fully qualified event anyway.
      ChanRecv cn :: PROCESS_NAME
cn v :: VAR
v s :: PROCESS_NAME
s r :: Range
r -> PROCESS_NAME -> VAR -> PROCESS_NAME -> Range -> EVENT
ChanRecv PROCESS_NAME
cn VAR
v PROCESS_NAME
s Range
r
      FQTermEvent t :: TERM ()
t r :: Range
r -> TERM () -> Range -> EVENT
TermEvent (TERM () -> TERM ()
simpCaslTerm TERM ()
t) Range
r
      FQExternalPrefixChoice fqVar :: TERM ()
fqVar r :: Range
r ->
        let (v :: VAR
v, s :: PROCESS_NAME
s) = TERM () -> (VAR, PROCESS_NAME)
splitCASLVar TERM ()
fqVar
        in VAR -> PROCESS_NAME -> Range -> EVENT
ExternalPrefixChoice VAR
v PROCESS_NAME
s Range
r
      FQInternalPrefixChoice fqVar :: TERM ()
fqVar r :: Range
r ->
        let (v :: VAR
v, s :: PROCESS_NAME
s) = TERM () -> (VAR, PROCESS_NAME)
splitCASLVar TERM ()
fqVar
        in VAR -> PROCESS_NAME -> Range -> EVENT
InternalPrefixChoice VAR
v PROCESS_NAME
s Range
r
      FQChanSend (cn :: PROCESS_NAME
cn, _) t :: TERM ()
t r :: Range
r -> PROCESS_NAME -> TERM () -> Range -> EVENT
ChanSend PROCESS_NAME
cn (TERM () -> TERM ()
simpCaslTerm TERM ()
t) Range
r
      FQChanNonDetSend (cn :: PROCESS_NAME
cn, _) fqVar :: TERM ()
fqVar r :: Range
r ->
        let (v :: VAR
v, s :: PROCESS_NAME
s) = TERM () -> (VAR, PROCESS_NAME)
splitCASLVar TERM ()
fqVar
        in PROCESS_NAME -> VAR -> PROCESS_NAME -> Range -> EVENT
ChanNonDetSend PROCESS_NAME
cn VAR
v PROCESS_NAME
s Range
r
      FQChanRecv (cn :: PROCESS_NAME
cn, _) fqVar :: TERM ()
fqVar r :: Range
r ->
        let (v :: VAR
v, s :: PROCESS_NAME
s) = TERM () -> (VAR, PROCESS_NAME)
splitCASLVar TERM ()
fqVar
        in PROCESS_NAME -> VAR -> PROCESS_NAME -> Range -> EVENT
ChanRecv PROCESS_NAME
cn VAR
v PROCESS_NAME
s Range
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 :: EVENT_SET -> EVENT_SET
simplifyEventSet eventSet :: EVENT_SET
eventSet = EVENT_SET
eventSet