content: {- |
  Module      :  ./CspCASLProver/TransProcesses.hs
  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
  