{- |
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 :: CspCASLSign -> Sign () () -> Sign () () -> VSM -> PROCESS -> Term
transProcess ccSign :: CspCASLSign
ccSign pcfolSign :: Sign () ()
pcfolSign cfolSign :: Sign () ()
cfolSign vsm :: VSM
vsm pr :: PROCESS
pr =
    let -- Make translations with all the signatures filled in
        transFormula' :: VSM -> FORMULA () -> Term
transFormula' = Sign () () -> Sign () () -> VSM -> FORMULA () -> Term
transFormula Sign () ()
pcfolSign Sign () ()
cfolSign
        transProcess' :: VSM -> PROCESS -> Term
transProcess' =
            CspCASLSign -> Sign () () -> Sign () () -> VSM -> PROCESS -> Term
transProcess CspCASLSign
ccSign Sign () ()
pcfolSign Sign () ()
cfolSign
        -- cspSign = ccSig2CspSign ccSign
        caslSign :: Sign () ()
caslSign = CspCASLSign -> Sign () ()
ccSig2CASLSign CspCASLSign
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 PROCESS
pr of
         -- precedence 0
         Skip _ -> Term
cspProver_skipOp
         Stop _ -> Term
cspProver_stopOp
         Div _ -> Term
cspProver_divOp
         -- Run -> App (cspProver_runOp) (head (transEventSet es)) NotCont
         Run _ _ -> String -> Term
conDouble "RunNotSupportedYet"
         -- Chaos -> App (cspProver_chaosOp) (head (transEventSet es)) NotCont
         Chaos _ _ -> String -> Term
conDouble "ChaosNotSupportedYet"
         NamedProcess fqpn :: FQ_PROCESS_NAME
fqpn fqParams :: [TERM ()]
fqParams _ ->
             let -- Make a process name term
                 pnTerm :: Term
pnTerm = String -> Term
conDouble (String -> Term) -> String -> Term
forall a b. (a -> b) -> a -> b
$ FQ_PROCESS_NAME -> String
convertFQProcessName2String FQ_PROCESS_NAME
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 (), b) -> Term
transParam (term :: TERM ()
term, _) =
                     let termTar :: TermTarget
termTar = SORT -> TermTarget
ChanSendOrParam (SORT -> TermTarget) -> SORT -> TermTarget
forall a b. (a -> b) -> a -> b
$
                                   String -> SORT
forall a. HasCallStack => String -> a
error "NYI: CspCASLProver.TransProcesses.transProcess: Not updated for new signatures yet" -- getProcParamSort pn (declaredSortIndex - 1)
                     in Sign () ()
-> Sign () () -> Sign () () -> VSM -> TermTarget -> TERM () -> Term
transCASLTerm Sign () ()
caslSign Sign () ()
pcfolSign Sign () ()
cfolSign
                        VSM
vsm TermTarget
termTar TERM ()
term
                 {- Create a list of translated parameters, we number the
                 parameters from one -}
                 paramTerms :: [Term]
paramTerms = ((TERM (), Int) -> Term) -> [(TERM (), Int)] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map (TERM (), Int) -> Term
forall b. (TERM (), b) -> Term
transParam ([(TERM (), Int)] -> [Term]) -> [(TERM (), Int)] -> [Term]
forall a b. (a -> b) -> a -> b
$ [TERM ()] -> [(TERM (), Int)]
forall a. [a] -> [(a, Int)]
number [TERM ()]
fqParams
             in Term -> Term
cspProver_NamedProcOp (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ if [TERM ()] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TERM ()]
fqParams
                -- If there are no parameters we just get the process name term
                then Term
pnTerm
                {- Otherwise we get the process name term applied to the
                parameters -}
                else (Term -> Term -> Term) -> Term -> [Term] -> Term
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Term -> Term -> Term
termAppl Term
pnTerm [Term]
paramTerms
         -- precedence 1
         ConditionalProcess fqFormula :: FORMULA ()
fqFormula p :: PROCESS
p q :: PROCESS
q _ ->
             Term -> Term -> Term -> Term
cspProver_conditionalOp (VSM -> FORMULA () -> Term
transFormula' VSM
vsm FORMULA ()
fqFormula)
                                         (VSM -> PROCESS -> Term
transProcess' VSM
vsm PROCESS
p)
                                         (VSM -> PROCESS -> Term
transProcess' VSM
vsm PROCESS
q)
         -- precedence 2
         Hiding {} -> String -> Term
conDouble "HidingNotSupportedYet"
             -- cspProver_hidingOp (transProcess' p) (union (transEventSet es))
         RenamingProcess {} -> String -> Term
conDouble "RenamingNotSupportedYet"
             {- cspProver_renamingOp (transProcess' p) (transRenaming re)
         precedence 3 -}
         Sequential p :: PROCESS
p q :: PROCESS
q _ ->
             Term -> Term -> Term
cspProver_sequenceOp (VSM -> PROCESS -> Term
transProcess' VSM
vsm PROCESS
p) (VSM -> PROCESS -> Term
transProcess' VSM
vsm PROCESS
q)
         PrefixProcess ev :: EVENT
ev p :: PROCESS
p _ ->
         -- All prefix events are dealt with inside the translation of events.
             CspCASLSign
-> Sign () () -> Sign () () -> VSM -> EVENT -> PROCESS -> Term
transEvent CspCASLSign
ccSign Sign () ()
pcfolSign Sign () ()
cfolSign VSM
vsm EVENT
ev PROCESS
p
         -- precedence 4
         InternalChoice p :: PROCESS
p q :: PROCESS
q _ ->
             Term -> Term -> Term
cspProver_internal_choiceOp (VSM -> PROCESS -> Term
transProcess' VSM
vsm PROCESS
p)
                                             (VSM -> PROCESS -> Term
transProcess' VSM
vsm PROCESS
q)
         ExternalChoice p :: PROCESS
p q :: PROCESS
q _ ->
             Term -> Term -> Term
cspProver_external_choiceOp (VSM -> PROCESS -> Term
transProcess' VSM
vsm PROCESS
p)
                                             (VSM -> PROCESS -> Term
transProcess' VSM
vsm PROCESS
q)
         -- precedence 5
         Interleaving p :: PROCESS
p q :: PROCESS
q _ ->
             Term -> Term -> Term
cspProver_interleavingOp (VSM -> PROCESS -> Term
transProcess' VSM
vsm PROCESS
p)
                                          (VSM -> PROCESS -> Term
transProcess' VSM
vsm PROCESS
q)
         SynchronousParallel p :: PROCESS
p q :: PROCESS
q _ ->
             Term -> Term -> Term
cspProver_synchronousOp (VSM -> PROCESS -> Term
transProcess' VSM
vsm PROCESS
p)
                                         (VSM -> PROCESS -> Term
transProcess' VSM
vsm PROCESS
q)
         GeneralisedParallel p :: PROCESS
p es :: EVENT_SET
es q :: PROCESS
q _ ->
             Term -> Term -> Term -> Term
cspProver_general_parallelOp (VSM -> PROCESS -> Term
transProcess' VSM
vsm PROCESS
p)
                                              (EVENT_SET -> Term
transEventSet EVENT_SET
es)
                                              (VSM -> PROCESS -> Term
transProcess' VSM
vsm PROCESS
q)

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

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

-- | Translate a fully qualified CommType into an Isabelle term.
transCommType :: CommType -> Term
transCommType :: CommType -> Term
transCommType comm :: CommType
comm =
    case CommType
comm of
      CommTypeSort sort :: SORT
sort -> SortTarget -> SORT -> Term
transSort SortTarget
NormalComm SORT
sort
      CommTypeChan typedChanName :: TypedChanName
typedChanName ->
          case TypedChanName
typedChanName of
            TypedChanName cn :: SORT
cn _ -> Term -> Term
rangeOp (String -> Term
conDouble (String -> Term) -> String -> Term
forall a b. (a -> b) -> a -> b
$ SORT -> String
convertChannelString SORT
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 :: CspCASLSign
-> Sign () () -> Sign () () -> VSM -> EVENT -> PROCESS -> Term
transEvent ccSign :: CspCASLSign
ccSign pcfolSign :: Sign () ()
pcfolSign cfolSign :: Sign () ()
cfolSign vsm :: VSM
vsm event :: EVENT
event p :: PROCESS
p =
    let -- Make translation with all the signatures filled in
        transProcess' :: VSM -> PROCESS -> Term
transProcess' = CspCASLSign -> Sign () () -> Sign () () -> VSM -> PROCESS -> Term
transProcess CspCASLSign
ccSign Sign () ()
pcfolSign Sign () ()
cfolSign
        caslSign :: Sign () ()
caslSign = CspCASLSign -> Sign () ()
ccSig2CASLSign CspCASLSign
ccSign
        transCASLTerm' :: VSM -> TermTarget -> TERM () -> Term
transCASLTerm' = Sign () ()
-> Sign () () -> Sign () () -> VSM -> TermTarget -> TERM () -> Term
transCASLTerm Sign () ()
caslSign Sign () ()
pcfolSign Sign () ()
cfolSign
    in case EVENT
event of
      FQTermEvent t :: TERM ()
t _ ->
        Term -> Term -> Term
cspProver_action_prefixOp (VSM -> TermTarget -> TERM () -> Term
transCASLTerm' VSM
vsm TermTarget
TermPrefix TERM ()
t)
        (VSM -> PROCESS -> Term
transProcess' VSM
vsm PROCESS
p)
      FQExternalPrefixChoice fqVar :: TERM ()
fqVar _ ->
        let (varName :: VAR
varName, varSort :: SORT
varSort) = TERM () -> (VAR, SORT)
splitCASLVar TERM ()
fqVar
        in Term -> Term -> Term -> Term
cspProver_internal_prefix_choiceOp (VAR -> Term
transVar VAR
varName)
           (SortTarget -> SORT -> Term
transSort SortTarget
NormalComm SORT
varSort)
           (VSM -> PROCESS -> Term
transProcess' (VAR -> VarSource -> VSM -> VSM
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert VAR
varName VarSource
PrefixChoice VSM
vsm) PROCESS
p)
      FQInternalPrefixChoice fqVar :: TERM ()
fqVar _ ->
        let (varName :: VAR
varName, varSort :: SORT
varSort) = TERM () -> (VAR, SORT)
splitCASLVar TERM ()
fqVar
        in Term -> Term -> Term -> Term
cspProver_external_prefix_choiceOp (VAR -> Term
transVar VAR
varName)
           (SortTarget -> SORT -> Term
transSort SortTarget
NormalComm SORT
varSort)
           (VSM -> PROCESS -> Term
transProcess' (VAR -> VarSource -> VSM -> VSM
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert VAR
varName VarSource
PrefixChoice VSM
vsm) PROCESS
p)
      FQChanSend (chanName :: SORT
chanName, chanSort :: SORT
chanSort) t :: TERM ()
t _ ->
        Term -> Term -> Term -> Term
cspProver_chan_sendOp (SORT -> Term
transChanName SORT
chanName)
        (VSM -> TermTarget -> TERM () -> Term
transCASLTerm' VSM
vsm (SORT -> TermTarget
ChanSendOrParam SORT
chanSort) TERM ()
t)
        (VSM -> PROCESS -> Term
transProcess' VSM
vsm PROCESS
p)
      FQChanNonDetSend (chanName :: SORT
chanName, chanSort :: SORT
chanSort) fqVar :: TERM ()
fqVar _ ->
        let declaredChanSort :: SORT
declaredChanSort = String -> Result SORT -> SORT
forall a. String -> Result a -> a
propagateErrors
                               "CspCASLProver.TransProcesses.transEvent1"
                               (Result SORT -> SORT) -> Result SORT -> SORT
forall a b. (a -> b) -> a -> b
$ (SORT, SORT) -> CspCASLSign -> Result SORT
getDeclaredChanSort (SORT
chanName, SORT
chanSort) CspCASLSign
ccSign
            (varName :: VAR
varName, varSort :: SORT
varSort) = TERM () -> (VAR, SORT)
splitCASLVar TERM ()
fqVar
        in Term -> Term -> Term -> Term -> Term
cspProver_chan_nondeterministic_sendOp (SORT -> Term
transChanName SORT
chanName)
           (VAR -> Term
transVar VAR
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. -}
           (SortTarget -> SORT -> Term
transSort (SORT -> SortTarget
ChanComm SORT
declaredChanSort) SORT
varSort)
           (VSM -> PROCESS -> Term
transProcess' (VAR -> VarSource -> VSM -> VSM
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert VAR
varName
                           (SORT -> VarSource
ChanSendOrRec SORT
declaredChanSort) VSM
vsm) PROCESS
p)
      FQChanRecv (chanName :: SORT
chanName, chanSort :: SORT
chanSort) fqVar :: TERM ()
fqVar _ ->
        let declaredChanSort :: SORT
declaredChanSort = String -> Result SORT -> SORT
forall a. String -> Result a -> a
propagateErrors
                               "CspCASLProver.TransProcesses.transEvent2"
                            (Result SORT -> SORT) -> Result SORT -> SORT
forall a b. (a -> b) -> a -> b
$ (SORT, SORT) -> CspCASLSign -> Result SORT
getDeclaredChanSort (SORT
chanName, SORT
chanSort) CspCASLSign
ccSign
            (varName :: VAR
varName, varSort :: SORT
varSort) = TERM () -> (VAR, SORT)
splitCASLVar TERM ()
fqVar
        in Term -> Term -> Term -> Term -> Term
cspProver_chan_recOp (SORT -> Term
transChanName SORT
chanName) (VAR -> Term
transVar VAR
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. -}
           (SortTarget -> SORT -> Term
transSort (SORT -> SortTarget
ChanComm SORT
declaredChanSort) SORT
varSort)
           (VSM -> PROCESS -> Term
transProcess' (VAR -> VarSource -> VSM -> VSM
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert VAR
varName
                           (SORT -> VarSource
ChanSendOrRec SORT
declaredChanSort) VSM
vsm) PROCESS
p)
      _ -> String -> Term
forall a. HasCallStack => String -> a
error (String -> Term) -> String -> Term
forall a b. (a -> b) -> a -> b
$ "CspCASLProver.TransProcesses.transEvent: "
                  String -> String -> String
forall a. [a] -> [a] -> [a]
++ "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 :: VAR -> Term
transVar v :: VAR
v = String -> Term
conDouble (String -> Term) -> String -> Term
forall a b. (a -> b) -> a -> b
$ VAR -> String
tokStr VAR
v

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

-- | Translated the channel name to Isabelle code.
transChanName :: CHANNEL_NAME -> Term
transChanName :: SORT -> Term
transChanName chanName :: SORT
chanName =
    String -> Term
conDouble (String -> Term) -> String -> Term
forall a b. (a -> b) -> a -> b
$ SORT -> String
convertChannelString SORT
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 :: Sign f e
-> Set String
-> FormulaTranslator f e
-> Set String
-> VSM
-> Record f Term Term
cspCaslTransRecord caslSign :: Sign f e
caslSign tyToks :: Set String
tyToks trForm :: FormulaTranslator f e
trForm strs :: Set String
strs vsm :: VSM
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. -}
    (Sign f e
-> Set String
-> FormulaTranslator f e
-> Set String
-> Record f Term Term
forall f e.
Sign f e
-> Set String
-> FormulaTranslator f e
-> Set String
-> Record f Term Term
CFOL2IsabelleHOL.transRecord Sign f e
caslSign Set String
tyToks FormulaTranslator f e
trForm Set String
strs)
    { foldQual_var :: TERM f -> VAR -> SORT -> Range -> Term
foldQual_var = \ _ v :: VAR
v s :: SORT
s _ ->
      let v' :: Term
v' = String -> Term
mkFree (String -> Term) -> String -> Term
forall a b. (a -> b) -> a -> b
$ Set String -> VAR -> String
CFOL2IsabelleHOL.transVar Set String
strs VAR
v
      in case VAR -> VSM -> Maybe VarSource
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup VAR
v VSM
vsm of
           Nothing ->
               String -> Term
forall a. HasCallStack => String -> a
error (String -> Term) -> String -> Term
forall a b. (a -> b) -> a -> b
$ "CspCASLProver.TransProcesses.cspCaslTransRecord: Variable not found in vsm:" String -> String -> String
forall a. [a] -> [a] -> [a]
++ VAR -> String
forall a. Show a => a -> String
show VAR
v
           Just varSource :: VarSource
varSource ->
               case VarSource
varSource of
                 PrefixChoice -> SORT -> Term -> Term
mkChooseFunOp SORT
s (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Term -> Term
projFlatOp Term
v'
                 ChanSendOrRec declaredChanSort :: SORT
declaredChanSort ->
                     SORT -> Term -> Term
mkChooseFunOp SORT
s (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ SORT -> Term -> Term
mkSortBarRepOp SORT
declaredChanSort Term
v'
                 GlobalParameter -> SORT -> Term -> Term
mkChooseFunOp SORT
s (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ SORT -> Term -> Term
mkSortBarRepOp SORT
s Term
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 :: Sign () ()
-> Sign () () -> Sign () () -> VSM -> TermTarget -> TERM () -> Term
transCASLTerm caslSign :: Sign () ()
caslSign pcfolSign :: Sign () ()
pcfolSign cfolSign :: Sign () ()
cfolSign vsm :: VSM
vsm termTarget :: TermTarget
termTarget caslTerm :: TERM ()
caslTerm =
    let strs :: Set String
strs = Sign () () -> Set String
forall f e. Sign f e -> Set String
CFOL2IsabelleHOL.getAssumpsToks Sign () ()
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 TERM ()
caslTerm of
         -- Variable
         CASL_AS_Basic_CASL.Qual_var v :: VAR
v s :: SORT
s _ ->
             let v' :: Term
v' = String -> Term
mkFree (String -> Term) -> String -> Term
forall a b. (a -> b) -> a -> b
$ Set String -> VAR -> String
CFOL2IsabelleHOL.transVar Set String
strs VAR
v
             in case TermTarget
termTarget of
               TermPrefix ->
                   case VAR -> VSM -> Maybe VarSource
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup VAR
v VSM
vsm of
                     Nothing -> String -> Term
forall a. HasCallStack => String -> a
error (String -> Term) -> String -> Term
forall a b. (a -> b) -> a -> b
$
                      "CspCASLProver.TransProcesses.transTerm: " String -> String -> String
forall a. [a] -> [a] -> [a]
++
                      "Variable not found in vsm:" String -> String -> String
forall a. [a] -> [a] -> [a]
++ VAR -> String
forall a. Show a => a -> String
show VAR
v
                     Just varSource :: VarSource
varSource ->
                         case VarSource
varSource of
                           PrefixChoice -> Term
v' -- the variable is already ok
                           ChanSendOrRec declaredChanSort :: SORT
declaredChanSort ->
                               Term -> Term
flatOp (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ SORT -> Term -> Term
mkSortBarRepOp SORT
declaredChanSort Term
v'
                           GlobalParameter -> Term -> Term
flatOp (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ SORT -> Term -> Term
mkSortBarRepOp SORT
s Term
v'
               ChanSendOrParam t :: SORT
t ->
                   case VAR -> VSM -> Maybe VarSource
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup VAR
v VSM
vsm of
                     Nothing -> String -> Term
forall a. HasCallStack => String -> a
error (String -> Term) -> String -> Term
forall a b. (a -> b) -> a -> b
$
                      "CspCASLProver.TransProcesses.transTerm: " String -> String -> String
forall a. [a] -> [a] -> [a]
++
                      "Variable not found in vsm:" String -> String -> String
forall a. [a] -> [a] -> [a]
++ VAR -> String
forall a. Show a => a -> String
show VAR
v
                     Just varSource :: VarSource
varSource ->
                         case VarSource
varSource of
                           PrefixChoice ->
                               SORT -> Term -> Term
mkSortBarAbsOp SORT
t (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Term -> Term
projFlatOp Term
v'
                           ChanSendOrRec declaredChanSort :: SORT
declaredChanSort ->
                               if SORT
declaredChanSort SORT -> SORT -> Bool
forall a. Eq a => a -> a -> Bool
== SORT
t
                               then Term
v'
                               else SORT -> Term -> Term
mkSortBarAbsOp SORT
t (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$
                                    SORT -> Term -> Term
mkSortBarRepOp SORT
declaredChanSort Term
v'
                           GlobalParameter ->
                               if SORT
s SORT -> SORT -> Bool
forall a. Eq a => a -> a -> Bool
== SORT
t
                               then Term
v'
                               else SORT -> Term -> Term
mkSortBarAbsOp SORT
t (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$
                                    SORT -> Term -> Term
mkSortBarRepOp SORT
s Term
v'
         -- Other (not a variable)
         _ -> let sort :: SORT
sort = TERM () -> SORT
forall f. TermExtension f => f -> SORT
CASL_Sign.sortOfTerm TERM ()
caslTerm
                  {- Make a Haskell function that will apply the constructor
                  around an Isabelle term. -}
                  constructor :: Term -> Term
constructor = SORT -> Term -> Term
mkPreAlphabetConstructorOp SORT
sort
                  {- Build the translation of the term wrapped in the
                  constructor wrapped in the class operation. -}
                  isaCaslTerm :: Term
isaCaslTerm = Term -> Term
classOp (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Term -> Term
constructor (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$
                                Sign () () -> Sign () () -> VSM -> TERM () -> Term
transCaslTermComputation Sign () ()
pcfolSign Sign () ()
cfolSign
                                                         VSM
vsm TERM ()
caslTerm
              in case TermTarget
termTarget of
                   TermPrefix -> Term -> Term
flatOp Term
isaCaslTerm
                   ChanSendOrParam t :: SORT
t -> SORT -> Term -> Term
mkSortBarAbsOp SORT
t Term
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 :: Sign () () -> Sign () () -> VSM -> TERM () -> Term
transCaslTermComputation pcfolSign :: Sign () ()
pcfolSign cfolSign :: Sign () ()
cfolSign vsm :: VSM
vsm term :: TERM ()
term =
    let -- Function to remove subsorting - from comorphism CASL2PCFOL
        rmSub :: TERM () -> TERM ()
rmSub = TERM () -> TERM ()
forall f. TermExtension f => TERM f -> TERM f
CASL2PCFOL.t2Term
        -- Remove subsorting from the term
        termNoSub :: TERM ()
termNoSub = TERM () -> TERM ()
rmSub TERM ()
term
        {- Function to remove partiality - from comorphism CASL2SubPCFOL
        This needs to match the translation CASL2SubCFOL.defaultCASL2SubCFOL -}
        b :: Bool
b = Bool
True {- We want unique bottom elements per sort
        Calculate the bottom sorts for the term and signature -}
        fbsrts :: Set SORT
fbsrts = TERM () -> Set SORT
forall f. TERM f -> Set SORT
CASL2SubCFOL.botTermSorts TERM ()
termNoSub
        bsrts :: Set SORT
bsrts = FormulaTreatment -> Sign () () -> Set SORT -> Set SORT
forall f e. FormulaTreatment -> Sign f e -> Set SORT -> Set SORT
CASL2SubCFOL.sortsWithBottom FormulaTreatment
CASL2SubCFOL.FormulaDependent
                Sign () ()
pcfolSign Set SORT
fbsrts
        rmPartial :: TERM () -> TERM ()
rmPartial = (() -> ()) -> TERM () -> TERM ()
forall f. Ord f => (f -> f) -> TERM f -> TERM f
CASL_Simplify.simplifyTerm () -> ()
forall a. a -> a
id (TERM () -> TERM ()) -> (TERM () -> TERM ()) -> TERM () -> TERM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
                    Bool -> Set SORT -> TERM () -> TERM ()
CASL2SubCFOL.codeTerm Bool
b Set SORT
bsrts
        {- Function to translate to Isabelle - from comorphism CFOL2IsabelleHOL
        We need the CFOL signature to translate the terms properly -}
        tyToks :: Set String
tyToks = Sign () () -> Set String
forall f e. Sign f e -> Set String
CFOL2IsabelleHOL.typeToks Sign () ()
cfolSign
        trForm :: FormulaTranslator () ()
trForm = FormulaTranslator () ()
CFOL2IsabelleHOL.formTrCASL
        strs :: Set String
strs = Sign () () -> Set String
forall f e. Sign f e -> Set String
CFOL2IsabelleHOL.getAssumpsToks Sign () ()
cfolSign
        toIsabelle :: TERM () -> Term
toIsabelle = Record () Term Term -> TERM () -> Term
forall f a b. Record f a b -> TERM f -> b
foldTerm (Record () Term Term -> TERM () -> Term)
-> Record () Term Term -> TERM () -> Term
forall a b. (a -> b) -> a -> b
$ Sign () ()
-> Set String
-> FormulaTranslator () ()
-> Set String
-> VSM
-> Record () Term Term
forall f e.
Sign f e
-> Set String
-> FormulaTranslator f e
-> Set String
-> VSM
-> Record f Term Term
cspCaslTransRecord Sign () ()
cfolSign
                     Set String
tyToks FormulaTranslator () ()
trForm Set String
strs VSM
vsm
        -- CFOL2IsabelleHOL.transFORMULA cfolSign tyToks trForm strs
    in TERM () -> Term
toIsabelle (TERM () -> Term) -> TERM () -> Term
forall a b. (a -> b) -> a -> b
$ TERM () -> TERM ()
rmPartial TERM ()
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 :: Sign () () -> Sign () () -> VSM -> FORMULA () -> Term
transFormula pcfolSign :: Sign () ()
pcfolSign cfolSign :: Sign () ()
cfolSign vsm :: VSM
vsm formula :: FORMULA ()
formula =
    let -- Function to remove subsorting - from comorphism CAS2PCFOL
        rmSub :: FORMULA () -> FORMULA ()
rmSub = FORMULA () -> FORMULA ()
forall f. TermExtension f => FORMULA f -> FORMULA f
CASL2PCFOL.f2Formula
        -- Remove subsorting from the formula
        formulaNoSub :: FORMULA ()
formulaNoSub = FORMULA () -> FORMULA ()
rmSub FORMULA ()
formula
        {- Function to remove partiality - from comorphism CAS2SubPCFOL
        This needs to match the translation CASL2SubCFOL.defaultCASL2SubCFOL -}
        b :: Bool
b = Bool
True {- We want unique bottom elements per sort
        Calculate the bottom sorts for the formula and signature -}
        fbsrts :: Set SORT
fbsrts = FORMULA () -> Set SORT
forall f. FORMULA f -> Set SORT
CASL2SubCFOL.botFormulaSorts FORMULA ()
formulaNoSub
        bsrts :: Set SORT
bsrts = FormulaTreatment -> Sign () () -> Set SORT -> Set SORT
forall f e. FormulaTreatment -> Sign f e -> Set SORT -> Set SORT
CASL2SubCFOL.sortsWithBottom FormulaTreatment
CASL2SubCFOL.FormulaDependent
                Sign () ()
pcfolSign Set SORT
fbsrts
        rmPartial :: FORMULA () -> FORMULA ()
rmPartial = (() -> ()) -> FORMULA () -> FORMULA ()
forall f. Ord f => (f -> f) -> FORMULA f -> FORMULA f
CASL_Simplify.simplifyFormula () -> ()
forall a. a -> a
id (FORMULA () -> FORMULA ())
-> (FORMULA () -> FORMULA ()) -> FORMULA () -> FORMULA ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
                    Bool -> Set SORT -> FORMULA () -> FORMULA ()
CASL2SubCFOL.codeFormula Bool
b Set SORT
bsrts
        {- Function to tranalate to Isabelle - from comorphism CFOL2IsabelleHOL
        We need the CFOL signature to translate the formula properly -}
        tyToks :: Set String
tyToks = Sign () () -> Set String
forall f e. Sign f e -> Set String
CFOL2IsabelleHOL.typeToks Sign () ()
cfolSign
        trForm :: FormulaTranslator () ()
trForm = FormulaTranslator () ()
CFOL2IsabelleHOL.formTrCASL
        strs :: Set String
strs = Sign () () -> Set String
forall f e. Sign f e -> Set String
CFOL2IsabelleHOL.getAssumpsToks Sign () ()
cfolSign
        toIsabelle :: FORMULA () -> Term
toIsabelle = Record () Term Term -> FORMULA () -> Term
forall f a b. Record f a b -> FORMULA f -> a
foldFormula (Record () Term Term -> FORMULA () -> Term)
-> Record () Term Term -> FORMULA () -> Term
forall a b. (a -> b) -> a -> b
$ Sign () ()
-> Set String
-> FormulaTranslator () ()
-> Set String
-> VSM
-> Record () Term Term
forall f e.
Sign f e
-> Set String
-> FormulaTranslator f e
-> Set String
-> VSM
-> Record f Term Term
cspCaslTransRecord Sign () ()
cfolSign
                     Set String
tyToks FormulaTranslator () ()
trForm Set String
strs VSM
vsm
        -- CFOL2IsabelleHOL.transFORMULA cfolSign tyToks trForm strs
    in FORMULA () -> Term
toIsabelle (FORMULA () -> Term) -> FORMULA () -> Term
forall a b. (a -> b) -> a -> b
$ FORMULA () -> FORMULA ()
rmPartial FORMULA ()
formulaNoSub