TransProcesses.hs

{- |
Module      :  $Header$
Description :  Provides transformations from Csp Processes to Isabelle terms
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

Provides translations from Csp Processes to Isabelle terms

-}
module CspCASLProver.TransProcesses
    ( transProcess
    , VarSource (..)
    ) where

import qualified CASL.AS_Basic_CASL as CASL_AS_Basic_CASL
import CASL.Fold as CASL_Fold
import qualified CASL.Sign as CASL_Sign
import qualified CASL.Simplify as CASL_Simplify

import Common.Id (tokStr)
import Common.Result (propagateErrors)
import Common.Utils (number)

import qualified Comorphisms.CASL2PCFOL as CASL2PCFOL
import qualified Comorphisms.CASL2SubCFOL as CASL2SubCFOL
import qualified Comorphisms.CFOL2IsabelleHOL as CFOL2IsabelleHOL

import CspCASL.AS_CspCASL_Process
import CspCASL.SignCSP (CspCASLSign, ccSig2CASLSign)

import CspCASL.StatAnaCSP (getDeclaredChanSort)

import CspCASLProver.Consts
import CspCASLProver.CspProverConsts

import qualified Data.Set as Set
import qualified Data.Map as Map

import Isabelle.IsaSign
import Isabelle.IsaConsts

-- | The origin of a variable
data VarSource
    -- | indicates that the variable originated from a prefix choice operator.
    = PrefixChoice
    {- | indicates that the variable originated from a channel nondeterministic
    send or channel receive where the sort is the declared sort of the
    channel. -}
    | ChanSendOrRec CASL_AS_Basic_CASL.SORT
    {- | indicates that the variable originated from global parameter to the
    process. -}
    | GlobalParameter

-- | The target of the sort translation
data SortTarget
    {- | Indicates the translated sort will be used as a normal communication
    e.g., as a prefix choice or event set. -}
    = NormalComm
    {- | Indicates that the sort will be used as a communication set with a
    channel of certain declared sort. -}
    | ChanComm CASL_AS_Basic_CASL.SORT

-- | The taraget of the term translation
data TermTarget
    -- | Indicates the term will be used in the term prefix operator
    = TermPrefix
    {- | Indicates that the term will be used either as a parameter (where sort
    is declared sort of the parameter) or as a channel communication (where
    the sort is the declared sort of the channel). -}
    | ChanSendOrParam CASL_AS_Basic_CASL.SORT

-- | Variable source map, which maps variables to the source of the variable.
type VSM = Map.Map CASL_AS_Basic_CASL.VAR VarSource

{- | 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. -}
transProcess :: CspCASLSign -> CASL_Sign.Sign () () ->
                CASL_Sign.Sign () () -> VSM -> PROCESS -> Term
transProcess ccSign pcfolSign cfolSign vsm pr =
    let -- Make translations with all the signatures filled in
        transFormula' = transFormula pcfolSign cfolSign
        transProcess' =
            transProcess ccSign pcfolSign cfolSign
        -- cspSign = ccSig2CspSign ccSign
        caslSign = ccSig2CASLSign ccSign
        {- getProcParamSort procName index =
        let procMap = procSet cspSign
        paramSortList = case Map.lookup procName procMap of
        Nothing -> error "CspCASLProver.TransProcesses.transProcess: Process name not found in process map."
        Just pp-> error "NYI: CspCASLProver.TransProcesses.transProcess: Not updated for new signatures yet" -- case pp of ProcProfile sorts _ -> sorts
        in paramSortList !! index -}
    in case pr of
         -- precedence 0
         Skip _ -> cspProver_skipOp
         Stop _ -> cspProver_stopOp
         Div _ -> cspProver_divOp
         -- Run -> App (cspProver_runOp) (head (transEventSet es)) NotCont
         Run _ _ -> conDouble "RunNotSupportedYet"
         -- Chaos -> App (cspProver_chaosOp) (head (transEventSet es)) NotCont
         Chaos _ _ -> conDouble "ChaosNotSupportedYet"
         NamedProcess fqpn fqParams _ ->
             let -- Make a process name term
                 pnTerm = conDouble $ convertFQProcessName2String fqpn
                 {- Translate an argument(a term), t is the sort of the declared
                 parameter (the sort of the variable may be a subsort of the
                 declared sort, so we must use the declared sort).
                 transParam (term, declaredSortIndex) = -}
                 transParam (term, _) =
                     let termTar = ChanSendOrParam $
                                   error "NYI: CspCASLProver.TransProcesses.transProcess: Not updated for new signatures yet" -- getProcParamSort pn (declaredSortIndex - 1)
                     in transCASLTerm caslSign pcfolSign cfolSign
                        vsm termTar term
                 {- Create a list of translated parameters, we number the
                 parameters from one -}
                 paramTerms = map transParam $ number fqParams
             in cspProver_NamedProcOp $ if null fqParams
                -- If there are no parameters we just get the process name term
                then pnTerm
                {- Otherwise we get the process name term applied to the
                parameters -}
                else foldl termAppl pnTerm paramTerms
         -- precedence 1
         ConditionalProcess fqFormula p q _ ->
             cspProver_conditionalOp (transFormula' vsm fqFormula)
                                         (transProcess' vsm p)
                                         (transProcess' vsm q)
         -- precedence 2
         Hiding {} -> conDouble "HidingNotSupportedYet"
             -- cspProver_hidingOp (transProcess' p) (union (transEventSet es))
         RenamingProcess {} -> conDouble "RenamingNotSupportedYet"
             {- cspProver_renamingOp (transProcess' p) (transRenaming re)
         precedence 3 -}
         Sequential p q _ ->
             cspProver_sequenceOp (transProcess' vsm p) (transProcess' vsm q)
         PrefixProcess ev p _ ->
         -- All prefix events are dealt with inside the translation of events.
             transEvent ccSign pcfolSign cfolSign vsm ev p
         -- precedence 4
         InternalChoice p q _ ->
             cspProver_internal_choiceOp (transProcess' vsm p)
                                             (transProcess' vsm q)
         ExternalChoice p q _ ->
             cspProver_external_choiceOp (transProcess' vsm p)
                                             (transProcess' vsm q)
         -- precedence 5
         Interleaving p q _ ->
             cspProver_interleavingOp (transProcess' vsm p)
                                          (transProcess' vsm q)
         SynchronousParallel p q _ ->
             cspProver_synchronousOp (transProcess' vsm p)
                                         (transProcess' vsm q)
         GeneralisedParallel p es q _ ->
             cspProver_general_parallelOp (transProcess' vsm p)
                                              (transEventSet es)
                                              (transProcess' vsm q)

         AlphabetisedParallel p les res q _ ->
             cspProver_alphabetised_parallelOp (transProcess' vsm p)
                                                   (transEventSet les)
                                                   (transEventSet res)
                                                   (transProcess' vsm q)
         {- Just forget the fully qualified data i.e. the constituent
         communication alphabet. Translate as normal. -}
         FQProcess p _ _ ->
             transProcess' vsm p

-- | Translate a fully qualified EventSet into a list Isabelle term.
transEventSet :: EVENT_SET -> Term
transEventSet (EventSet comms _) =
  if null comms then error "transEventSet" else
          {- This list will not be empty otherwise, if it was empty the static
          analysis would have failed. -}
          foldr1 binUnion (map transCommType comms)

-- | Translate a fully qualified CommType into an Isabelle term.
transCommType :: CommType -> Term
transCommType comm =
    case comm of
      CommTypeSort sort -> transSort NormalComm sort
      CommTypeChan typedChanName ->
          case typedChanName of
            TypedChanName cn _ -> rangeOp (conDouble $ convertChannelString cn)

{- | Translate a process event into CspProver (Isabelle). We need to know the
data part (CASL signature) in order to use the same translation for CASL
terms as the data encoding into Isabelle did. We need the Csp signature for
getting the declared channel sorts. 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. We need the vsm to pass it on to the term
translation. -}
transEvent :: CspCASLSign -> CASL_Sign.Sign () () ->
              CASL_Sign.Sign () () -> VSM ->
              EVENT -> PROCESS -> Term
transEvent ccSign pcfolSign cfolSign vsm event p =
    let -- Make translation with all the signatures filled in
        transProcess' = transProcess ccSign pcfolSign cfolSign
        caslSign = ccSig2CASLSign ccSign
        transCASLTerm' = transCASLTerm caslSign pcfolSign cfolSign
    in case event of
      FQTermEvent t _ ->
        cspProver_action_prefixOp (transCASLTerm' vsm TermPrefix t)
        (transProcess' vsm p)
      FQExternalPrefixChoice fqVar _ ->
        let (varName, varSort) = splitCASLVar fqVar
        in cspProver_internal_prefix_choiceOp (transVar varName)
           (transSort NormalComm varSort)
           (transProcess' (Map.insert varName PrefixChoice vsm) p)
      FQInternalPrefixChoice fqVar _ ->
        let (varName, varSort) = splitCASLVar fqVar
        in cspProver_external_prefix_choiceOp (transVar varName)
           (transSort NormalComm varSort)
           (transProcess' (Map.insert varName PrefixChoice vsm) p)
      FQChanSend (chanName, chanSort) t _ ->
        cspProver_chan_sendOp (transChanName chanName)
        (transCASLTerm' vsm (ChanSendOrParam chanSort) t)
        (transProcess' vsm p)
      FQChanNonDetSend (chanName, chanSort) fqVar _ ->
        let declaredChanSort = propagateErrors
                               "CspCASLProver.TransProcesses.transEvent1"
                               $ getDeclaredChanSort (chanName, chanSort) ccSign
            (varName, varSort) = splitCASLVar fqVar
        in cspProver_chan_nondeterministic_sendOp (transChanName chanName)
           (transVar varName)
           {- The translate sort (channel version) of the set to receive
           from. Note that the sort is the sort of the variable as specified,
           we want here the declaration sort of the channel. -}
           (transSort (ChanComm declaredChanSort) varSort)
           (transProcess' (Map.insert varName
                           (ChanSendOrRec declaredChanSort) vsm) p)
      FQChanRecv (chanName, chanSort) fqVar _ ->
        let declaredChanSort = propagateErrors
                               "CspCASLProver.TransProcesses.transEvent2"
                            $ getDeclaredChanSort (chanName, chanSort) ccSign
            (varName, varSort) = splitCASLVar fqVar
        in cspProver_chan_recOp (transChanName chanName) (transVar varName)
           {- The translate sort (channel version) of the set to receive
           from. Note that the sort is the sort of the variable as specified,
           we want here the declaration sort of the channel. -}
           (transSort (ChanComm declaredChanSort) varSort)
           (transProcess' (Map.insert varName
                           (ChanSendOrRec declaredChanSort) vsm) p)
      _ -> error $ "CspCASLProver.TransProcesses.transEvent: "
                  ++ "Expected a FQEvent not a non-FQEvent"

{- | Translate a variable into CspProver (Isabelle). Notice
that this does not work on fully qualified CASL variables (TERMs)
but instead on VAR. -}
transVar :: CASL_AS_Basic_CASL.VAR -> Term
transVar v = conDouble $ tokStr v

{- | Translate a sort into CspProver (Isabelle) depending on the target of the
sort. -}
transSort :: SortTarget -> CASL_AS_Basic_CASL.SORT -> Term
transSort target s =
    let sBar = conDouble $ mkSortBarString s
    in case target of
         NormalComm -> binImageOp (conDouble flatS) sBar
         ChanComm t -> binImageOp
                       (conDouble $ mkSortBarAbsString t) sBar

-- | Translated the channel name to Isabelle code.
transChanName :: CHANNEL_NAME -> Term
transChanName chanName =
    conDouble $ convertChannelString chanName

{- transRenaming :: RENAMING -> Term
transRenaming _ = conDouble "RenamingNotDoneYet" -}

{- -----------------------------------------------------------------------
Functions the translations of CASL terms and formulae               --
----------------------------------------------------------------------- -}

{- | Produce a record that is used to translate CASL terms and formulae to
Isabelle Terms. This record is the same as the CFOL2IsabelleHOL.transRecord
but deals with variables by applying a case on the origin of the
variable. The Isabelle terms produced when this record is used are always
of basic types i.e., can be used as parameters for function in the data
encoding. -}
cspCaslTransRecord :: CASL_Sign.Sign f e -> Set.Set String ->
                      CFOL2IsabelleHOL.FormulaTranslator f e ->
                      Set.Set String -> VSM -> Record f Term Term
cspCaslTransRecord caslSign tyToks trForm strs vsm =
     {- We use the existing record for translation but change its
     function in the case of a qualified variable. If we have a
     variable then we must make a translate the variable but wrap it in the
     correct choose function for it's sort. -}
    (CFOL2IsabelleHOL.transRecord caslSign tyToks trForm strs)
    { foldQual_var = \ _ v s _ ->
      let v' = mkFree $ CFOL2IsabelleHOL.transVar strs v
      in case Map.lookup v vsm of
           Nothing ->
               error $ "CspCASLProver.TransProcesses.cspCaslTransRecord: Variable not found in vsm:" ++ show v
           Just varSource ->
               case varSource of
                 PrefixChoice -> mkChooseFunOp s $ projFlatOp v'
                 ChanSendOrRec declaredChanSort ->
                     mkChooseFunOp s $ mkSortBarRepOp declaredChanSort v'
                 GlobalParameter -> mkChooseFunOp s $ mkSortBarRepOp s v'
    }

{- | Translate a CASL term into an Isabelle term. The result of this function
depends on the term target. a target of TermPrefix indicates we must land
in the alphabet and have a flat constructor wrapped around the
translation. A ChanSendOrParam indicates that the translated term will be
used in a channel send operator or as a parameter to a named process. The
translation also changes depending on the source of the variables used. -}
transCASLTerm :: CASL_Sign.Sign () () -> CASL_Sign.Sign () () ->
                 CASL_Sign.Sign () () -> VSM -> TermTarget ->
                 CASL_AS_Basic_CASL.TERM () -> Term
transCASLTerm caslSign pcfolSign cfolSign vsm termTarget caslTerm =
    let strs = CFOL2IsabelleHOL.getAssumpsToks caslSign
    {- We make a case on the type of term, then on the term target, then if we
    have a variable we make a case on the source of the variable -}
    in case caslTerm of
         -- Variable
         CASL_AS_Basic_CASL.Qual_var v s _ ->
             let v' = mkFree $ CFOL2IsabelleHOL.transVar strs v
             in case termTarget of
               TermPrefix ->
                   case Map.lookup v vsm of
                     Nothing -> error $
                      "CspCASLProver.TransProcesses.transTerm: " ++
                      "Variable not found in vsm:" ++ show v
                     Just varSource ->
                         case varSource of
                           PrefixChoice -> v' -- the variable is already ok
                           ChanSendOrRec declaredChanSort ->
                               flatOp $ mkSortBarRepOp declaredChanSort v'
                           GlobalParameter -> flatOp $ mkSortBarRepOp s v'
               ChanSendOrParam t ->
                   case Map.lookup v vsm of
                     Nothing -> error $
                      "CspCASLProver.TransProcesses.transTerm: " ++
                      "Variable not found in vsm:" ++ show v
                     Just varSource ->
                         case varSource of
                           PrefixChoice ->
                               mkSortBarAbsOp t $ projFlatOp v'
                           ChanSendOrRec declaredChanSort ->
                               if declaredChanSort == t
                               then v'
                               else mkSortBarAbsOp t $
                                    mkSortBarRepOp declaredChanSort v'
                           GlobalParameter ->
                               if s == t
                               then v'
                               else mkSortBarAbsOp t $
                                    mkSortBarRepOp s v'
         -- Other (not a variable)
         _ -> let sort = CASL_Sign.sortOfTerm caslTerm
                  {- Make a Haskell function that will apply the constructor
                  around an Isabelle term. -}
                  constructor = mkPreAlphabetConstructorOp sort
                  {- Build the translation of the term wrapped in the
                  constructor wrapped in the class operation. -}
                  isaCaslTerm = classOp $ constructor $
                                transCaslTermComputation pcfolSign cfolSign
                                                         vsm caslTerm
              in case termTarget of
                   TermPrefix -> flatOp isaCaslTerm
                   ChanSendOrParam t -> mkSortBarAbsOp t isaCaslTerm

{- | Translate a CASL Term to an Isabelle Term using the exact translation as is
done in the comorphism composition
CASL2PCFOL;defaultCASL2SubCFOL;CFOL2IsabelleHOL with out customised
variable translation (see cspCaslTransRecord for where that customisation
is define). The resulting Isabelle term of this function will be of the
underlying sort types, thus can be used as parameters of CASL functions in
the data part. We need the PCFOL and CFOL signature of the data part after
translation to CFOL to translate the formula. -}
transCaslTermComputation :: CASL_Sign.Sign () () -> CASL_Sign.Sign () () ->
                            VSM -> CASL_AS_Basic_CASL.TERM () -> Term
transCaslTermComputation pcfolSign cfolSign vsm term =
    let -- Function to remove subsorting - from comorphism CASL2PCFOL
        rmSub = CASL2PCFOL.t2Term
        -- Remove subsorting from the term
        termNoSub = rmSub term
        {- Function to remove partiality - from comorphism CASL2SubPCFOL
        This needs to match the translation CASL2SubCFOL.defaultCASL2SubCFOL -}
        b = True {- We want unique bottom elements per sort
        Calculate the bottom sorts for the term and signature -}
        fbsrts = CASL2SubCFOL.botTermSorts termNoSub
        bsrts = CASL2SubCFOL.sortsWithBottom CASL2SubCFOL.FormulaDependent
                pcfolSign fbsrts
        rmPartial = CASL_Simplify.simplifyTerm id .
                    CASL2SubCFOL.codeTerm b bsrts
        {- Function to translate to Isabelle - from comorphism CFOL2IsabelleHOL
        We need the CFOL signature to translate the terms properly -}
        tyToks = CFOL2IsabelleHOL.typeToks cfolSign
        trForm = CFOL2IsabelleHOL.formTrCASL
        strs = CFOL2IsabelleHOL.getAssumpsToks cfolSign
        toIsabelle = foldTerm $ cspCaslTransRecord cfolSign
                     tyToks trForm strs vsm
        -- CFOL2IsabelleHOL.transFORMULA cfolSign tyToks trForm strs
    in toIsabelle $ rmPartial termNoSub

{- | Translate a fully qualified CASL formula into an Isabelle Term using the
exact translation as is done in the comorphism composition
CASL2PCFOL;defaultCASL2SubCFOL;CFOL2IsabelleHOL except translate CASL terms
using the CASL term translation for computation, where the terms will be
translated such that they are of the underlying sort types and thus can be
used as operands to the formula operators. -}
transFormula :: CASL_Sign.Sign () () -> CASL_Sign.Sign () () -> VSM ->
                CASL_AS_Basic_CASL.FORMULA () -> Term
transFormula pcfolSign cfolSign vsm formula =
    let -- Function to remove subsorting - from comorphism CAS2PCFOL
        rmSub = CASL2PCFOL.f2Formula
        -- Remove subsorting from the formula
        formulaNoSub = rmSub formula
        {- Function to remove partiality - from comorphism CAS2SubPCFOL
        This needs to match the translation CASL2SubCFOL.defaultCASL2SubCFOL -}
        b = True {- We want unique bottom elements per sort
        Calculate the bottom sorts for the formula and signature -}
        fbsrts = CASL2SubCFOL.botFormulaSorts formulaNoSub
        bsrts = CASL2SubCFOL.sortsWithBottom CASL2SubCFOL.FormulaDependent
                pcfolSign fbsrts
        rmPartial = CASL_Simplify.simplifyFormula id .
                    CASL2SubCFOL.codeFormula b bsrts
        {- Function to tranalate to Isabelle - from comorphism CFOL2IsabelleHOL
        We need the CFOL signature to translate the formula properly -}
        tyToks = CFOL2IsabelleHOL.typeToks cfolSign
        trForm = CFOL2IsabelleHOL.formTrCASL
        strs = CFOL2IsabelleHOL.getAssumpsToks cfolSign
        toIsabelle = foldFormula $ cspCaslTransRecord cfolSign
                     tyToks trForm strs vsm
        -- CFOL2IsabelleHOL.transFORMULA cfolSign tyToks trForm strs
    in toIsabelle $ rmPartial formulaNoSub