content: {- |
  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 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
  