Changeset 12792

Timestamp:

06.11.2009 14:50:45 (2 weeks ago)

Author:

csliam

Message:

Added Isabelle functions Image and Range. Drastically changed how the
process translation works. It now works for channels and term prefix
in a compatible way. All channel operations are now supported by
CspCASLProver. Renaming, hiding, chaos and run are still not supported.

Location:

trunk

Files:

• CspCASLProver/Consts.hs (modified) (10 diffs)
• CspCASLProver/CspCASLProver.hs (modified) (1 diff)
• CspCASLProver/CspProverConsts.hs (modified) (3 diffs)
• CspCASLProver/TransProcesses.hs (modified) (15 diffs)
• CspCASLProver/Utils.hs (modified) (11 diffs)
• Isabelle/IsaConsts.hs (modified) (4 diffs)

trunk/CspCASLProver/Consts.hs

@@ -20 +20 @@
     , classOp
     , classS
+    , convertChannelString
     , convertProcessName2String
     , convertSort2String
@@ -30 +31 @@
     , eventType
     , flatS
+    , flatOp
     , preAlphabetQuotType
     , preAlphabetS
@@ -35 +37 @@
     , preAlphabetType
     , projFlatS
+     , projFlatOp
     , mkChooseFunName
     , mkChooseFunOp
     , mkCompareWithFunName
-    , mkEventChannelConstructor
     , mkPreAlphabetConstructor
     , mkPreAlphabetConstructorOp
     , mkProcNameConstructor
+    , mkSortBarAbsString
     , mkSortBarAbsOp
     , mkSortBarRepOp
     , mkSortBarString
     , mkSortBarType
-    , mkSortDataSetString
     , mkSortFlatString
     , mkThyNameAlphabet
@@ -101 +103 @@
 classS = "class"
 
+-- | Function that takes a channel name produces the
+--   CspCASLProver's constructor for that channel.
+convertChannelString :: CHANNEL_NAME -> String
+convertChannelString = show
+
 -- | Convert a SORT to a string
 convertSort2String :: SORT -> String
@@ -112 +119 @@
 cspFThyS :: String
 cspFThyS  = "CSP_F"
-
--- | The string to use for the names of the data set types. See the channel
---   construction and the event data type.
-dataSetS :: String
-dataSetS = "DataSet"
 
 -- | String of the name of the function to compare eqaulity of two
@@ -154 +156 @@
 flatS = "Flat"
 
+-- | Function that takes a Term and adds a flat around it
+flatOp :: Term -> Term
+flatOp = termAppl (conDouble flatS)
+
 -- | Function that takes a sort and outputs the function name for the
 --   corresponing choose function
@@ -168 +174 @@
 mkCompareWithFunName :: SORT -> String
 mkCompareWithFunName sort = ("compare_with_" ++ (mkPreAlphabetConstructor sort))
-
--- | Function that takes a channel name and a target sort and produces the
---   CspCASLProver's constructor for that channel with that target sort.
-mkEventChannelConstructor :: CHANNEL_NAME -> SORT -> String
-mkEventChannelConstructor c s = (show c) ++ "_" ++ (convertSort2String s)
 
 -- | Function that returns the constructor of PreAlphabet for a given
@@ -199 +200 @@
 mkSortBarType sort = Type {typeId = (mkSortBarString sort), typeSort = [], typeArgs =[]}
 
--- | Converts a sort in to the corresponding Data Set type for that sort
--- represented as a string. This is used in the construction of the channels and
--- is linked with the type event.
-mkSortDataSetString :: SORT -> String
-mkSortDataSetString s = (convertSort2String s) ++ "_" ++ dataSetS
+-- | Given a sort this function produces the function name (string) of the built
+--   in Isabelle fucntion that corresponds to the abstraction function of the
+--   type that sort_bar.
+mkSortBarAbsString :: SORT -> String
+mkSortBarAbsString s = "Abs_" ++ convertSort2String s ++ barExtS
+
+-- | Given a sort this function produces the a function on the abstract syntax
+--   of Isabelle that represents the built in Isabelle fucntion that corresponds
+--   to the abstraction function of the type sort_bar.
+mkSortBarAbsOp :: SORT -> Term -> Term
+mkSortBarAbsOp s = termAppl (conDouble (mkSortBarAbsString s))
+
+-- | Given a sort this function produces the function name (string) of the built
+--   in Isabelle fucntion that corresponds to the representation function of the
+--   type sort_bar.
+mkSortBarRepString :: SORT -> String
+mkSortBarRepString s = "Rep_" ++ convertSort2String s ++ barExtS
+
+-- | Given a sort this function produces the a function on the abstract syntax
+--   of Isabelle that represents the built in Isabelle fucntion that corresponds
+--   to the representation function of the type sort_bar.
+mkSortBarRepOp :: SORT -> Term -> Term
+mkSortBarRepOp s = termAppl (conDouble (mkSortBarRepString s))
 
 -- | Converts asort in to the corresponding flat type for that sort represented
@@ -211 +230 @@
 mkSortFlatString s = (convertSort2String s) ++ "_" ++ flatS
 
--- | Given a sort this function produces the function name (string) of the built
---   in Isabelle fucntion that corresponds to the abstraction function of the
---   type that sort_bar.
-mkSortBarAbsString :: SORT -> String
-mkSortBarAbsString s = "Abs_" ++ convertSort2String s ++ barExtS
-
--- | Given a sort this function produces the a function on the abstract syntax
---   of Isabelle that represents the built in Isabelle fucntion that corresponds
---   to the abstraction function of the type sort_bar.
-mkSortBarAbsOp :: SORT -> Term -> Term
-mkSortBarAbsOp s = termAppl (conDouble (mkSortBarAbsString s))
-
--- | Given a sort this function produces the function name (string) of the built
---   in Isabelle fucntion that corresponds to the representation function of the
---   type sort_bar.
-mkSortBarRepString :: SORT -> String
-mkSortBarRepString s = "Rep_" ++ convertSort2String s ++ barExtS
-
--- | Given a sort this function produces the a function on the abstract syntax
---   of Isabelle that represents the built in Isabelle fucntion that corresponds
---   to the representation function of the type sort_bar.
-mkSortBarRepOp :: SORT -> Term -> Term
-mkSortBarRepOp s = termAppl (conDouble (mkSortBarRepString s))
-
 -- | Created a name for the theory file which stores the alphabet
 --   construction for CspCASLProver.
@@ -303 +298 @@
 projFlatS = "projFlat"
 
+-- | Apply the CspCASLProvers projFlat function to an isabelle term
+projFlatOp :: Term -> Term
+projFlatOp = termAppl (conDouble projFlatS)
+
 -- | Name for IsabelleHOL quot type
 quotS :: String

trunk/CspCASLProver/CspCASLProver.hs

@@ -201 +201 @@
         -- Start with our empty isabelle theory and add the
         -- processes the the process refinement theorems.
-        (isaSign, isaSens) = addProcMap ccNnamedSens caslSign pcfolSign cfolSign
+        (isaSign, isaSens) = addProcMap ccNnamedSens ccSign pcfolSign cfolSign
                            $ addProcNameDatatype cspSign
-                           $ addDataSetTypes sortList
                            $ addFlatTypes sortList
                            $ addProjFlatFun

trunk/CspCASLProver/CspProverConsts.hs

@@ -34 +34 @@
     , cspProver_conditionalOp
     , cspProver_chan_nondeterministic_sendOp
+    , cspProver_chan_sendOp
+    , cspProver_chan_recOp
 ) where
 
@@ -212 +214 @@
 cspProver_chan_nondeterministic_sendAltArgOpPrio = 80
 
+-- | Channel send operator symbols
+cspProver_chan_sendS :: String
+cspProver_chan_sendS = "Send_prefix"
+cspProver_chan_sendAltS :: String
+cspProver_chan_sendAltS = "(_ ! _ -> _)"
+cspProver_chan_sendAltArgPrios :: [Int]
+cspProver_chan_sendAltArgPrios = [900,1000,80]
+cspProver_chan_sendAltArgOpPrio :: Int
+cspProver_chan_sendAltArgOpPrio = 80
+
+-- | Channel receive operator symbols
+cspProver_chan_recS :: String
+cspProver_chan_recS = "Rec_prefix"
+cspProver_chan_recAltS :: String
+cspProver_chan_recAltS = "(_ ? _ : _ -> _)"
+cspProver_chan_recAltArgPrios :: [Int]
+cspProver_chan_recAltArgPrios = [900,900,1000,80]
+cspProver_chan_recAltArgOpPrio :: Int
+cspProver_chan_recAltArgOpPrio = 80
+
 -- Isabelle Terms representing the operations for CspProver
 
@@ -354 +376 @@
                         cspProver_chan_nondeterministic_sendAltArgOpPrio
 
-
+-- | Channel send operator
+cspProver_chan_sendOp :: Term -> Term -> Term -> Term
+cspProver_chan_sendOp  =
+    makeTriCspProverOp cspProver_chan_sendS
+                       cspProver_chan_sendAltS
+                       cspProver_chan_sendAltArgPrios
+                       cspProver_chan_sendAltArgOpPrio
+
+-- | Channel receive operator
+cspProver_chan_recOp :: Term -> Term -> Term -> Term -> Term
+cspProver_chan_recOp  =
+    makeQuadCspProverOp cspProver_chan_recS
+                        cspProver_chan_recAltS
+                        cspProver_chan_recAltArgPrios
+                        cspProver_chan_recAltArgOpPrio
 
 -- | Create an Isabelle Term representing a (Unary) CspProver operator

trunk/CspCASLProver/TransProcesses.hs

@@ -15 +15 @@
 module CspCASLProver.TransProcesses
     ( transProcess
+    , VarSource(..)
     )where
 
@@ -29 +30 @@
 
 import CspCASL.AS_CspCASL_Process
-import CspCASL.SignCSP (FQProcVarList)
+import CspCASL.SignCSP (CspCASLSign, CspSign(..),
+                        ccSig2CASLSign, ccSig2CspSign, ProcProfile(..))
 
 import CspCASLProver.Consts
@@ -35 +37 @@
 
 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
@@ -44 +82 @@
 --   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 :: CASL_Sign.Sign () () -> CASL_Sign.Sign () () ->
-                CASL_Sign.Sign () () -> FQProcVarList -> PROCESS -> Term
-transProcess caslSign pcfolSign cfolSign globalVars pr =
+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 globalVars
-        transProcess' = transProcess caslSign pcfolSign cfolSign globalVars
-        -- Union all the event sets together in Isabelle using the Isabelle
-        -- binary union operator
-        union esList = foldr1 binUnion esList
+        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 -> case pp of
+                                          ProcProfile sorts _ -> sorts
+            in paramSortList !! index
     in case pr of
          -- precedence 0
@@ -58 +103 @@
          Stop _ -> cspProver_stopOp
          Div  _ -> cspProver_divOp
-         Run es _ -> App (cspProver_runOp) (head (transEventSet es)) NotCont
-         Chaos es _ -> App (cspProver_chaosOp) (head (transEventSet es)) NotCont
+         -- Run -> App (cspProver_runOp) (head (transEventSet es)) NotCont
+         Run _ _ -> conDouble "RunNotSupportedYet"
+         -- Chaos -> App (cspProver_chaosOp) (head (transEventSet es)) NotCont
+         Chaos _ _ -> conDouble "ChaosNotSupportedYet"
          NamedProcess pn fqParams _ ->
              let -- Make a process name term
                  pnTerm = conDouble $ convertProcessName2String pn
-                 -- Translate an argument(a term) as normal but make sure
-                 -- we land in the bar types and not in the alphabet
-                 transParam t = transTerm False caslSign pcfolSign cfolSign
-                                globalVars t
-                 -- Create a list of translated parameters
-                 paramTerms = map transParam fqParams
+                 -- 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) =
+                     let termTar = ChanSendOrParam $
+                                   getProcParamSort pn declaredSortIndex
+                     in transCASLTerm caslSign pcfolSign cfolSign
+                        vsm termTar term
+                 -- Create a list of translated parameters, we number the
+                 -- parameters from zero
+                 paramTerms = map transParam $ zip fqParams [0..]
              in if (null fqParams)
                 -- If there are no parameters we just get the process name term
@@ -77 +129 @@
          -- precedence 1
          ConditionalProcess fqFormula p q _ ->
-             cspProver_conditionalOp (transFormula' fqFormula) (transProcess' p)
-                                         (transProcess' q)
+             cspProver_conditionalOp (transFormula' vsm fqFormula)
+                                         (transProcess' vsm p)
+                                         (transProcess' vsm q)
          -- precedence 2
-         Hiding p es _ ->
-             cspProver_hidingOp (transProcess' p) (union (transEventSet es))
-         RenamingProcess p re _ ->
-             cspProver_renamingOp (transProcess' p) (transRenaming re)
+         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' p) (transProcess' q)
+             cspProver_sequenceOp (transProcess' vsm p) (transProcess' vsm q)
          PrefixProcess ev p _ ->
          -- All prefix events are dealt with inside the translation of events.
-             transEvent caslSign pcfolSign cfolSign globalVars ev p
+             transEvent ccSign pcfolSign cfolSign vsm ev p
          -- precedence 4
          InternalChoice p q _ ->
-             cspProver_internal_choiceOp (transProcess' p) (transProcess'  q)
+             cspProver_internal_choiceOp (transProcess' vsm p)
+                                             (transProcess' vsm q)
          ExternalChoice p q _ ->
-             cspProver_external_choiceOp (transProcess' p) (transProcess'  q)
+             cspProver_external_choiceOp (transProcess' vsm p)
+                                             (transProcess' vsm q)
          -- precedence 5
          Interleaving p q _ ->
-             cspProver_interleavingOp (transProcess' p) (transProcess' q)
+             cspProver_interleavingOp (transProcess' vsm p)
+                                          (transProcess' vsm q)
          SynchronousParallel p q _ ->
-             cspProver_synchronousOp (transProcess' p) (transProcess' q)
+             cspProver_synchronousOp (transProcess' vsm p)
+                                         (transProcess' vsm q)
          GeneralisedParallel p es q _ ->
-             cspProver_general_parallelOp (transProcess' p)
-                                              (union (transEventSet es))
-                                              (transProcess'  q)
+             cspProver_general_parallelOp (transProcess' vsm p)
+                                              (transEventSet es)
+                                              (transProcess' vsm  q)
 
          AlphabetisedParallel p les res q _ ->
-             cspProver_alphabetised_parallelOp (transProcess' p)
-                                                   (union (transEventSet les))
-                                                   (union (transEventSet res))
-                                                   (transProcess'  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'  p
-
--- | Translate a fully qualified EventSet into a list Isabelle term.  Event Sets
---   are treated differently in different CSP operators, so its up to the
---   calling function to do somehting useful with the returned list.
-transEventSet :: EVENT_SET -> [Term]
+             transProcess' vsm p
+
+-- | Translate a fully qualified EventSet into a list Isabelle term.
+transEventSet :: EVENT_SET -> Term
 transEventSet evs =
     case evs of
-      EventSet _ _ -> error "CspCASLProver.TransProcesses.transEventSet: Expected a FQEventSet not a non-FQEventSet";
-      FQEventSet comms _ -> map transCommType comms
+      EventSet _ _ ->
+          error "CspCASLProver.TransProcesses.transEventSet: Expected a FQEventSet not a non-FQEventSet";
+      FQEventSet comms _ ->
+          -- 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.
@@ -128 +187 @@
 transCommType comm =
     case comm of
-      CommTypeSort sort -> conDouble $ mkSortBarString sort
+      CommTypeSort sort -> transSort NormalComm sort
       CommTypeChan typedChanName ->
           case typedChanName of
-            TypedChanName _ _ ->
-                error "CspCASLProver.TransProcesses.transCommType: Typed channel name translation not implemented"
+            TypedChanName cn _ -> rangeOp (conDouble $ convertChannelString cn)
 
 -- | Translate a process event into CspProver (Isabelle). We need to know the
---   data pat (CASL signature) inorder to use the same translation for CASL
---   terms as the data encoding into Isabelle did. 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.
-transEvent :: CASL_Sign.Sign () () -> CASL_Sign.Sign () () ->
-              CASL_Sign.Sign () () -> FQProcVarList ->
+--   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 caslSign pcfolSign cfolSign globalVars event p =
+transEvent ccSign pcfolSign cfolSign vsm event p =
     let -- Make translation with all the signatures filled in
-        transProcess' = transProcess caslSign pcfolSign cfolSign globalVars
+        transProcess' = transProcess ccSign pcfolSign cfolSign
+        chanMap = chans $ ccSig2CspSign ccSign
+        caslSign = ccSig2CASLSign ccSign
+        transCASLTerm' = transCASLTerm caslSign pcfolSign cfolSign
     in case event of
       -- To use the fully qualified data we need to know what the underlying
@@ -152 +214 @@
           case ev of
             TermEvent _ _ ->
-                -- Translate the term and make sure we do land in the
-                -- alphabet and not in the bar types
-                cspProver_action_prefixOp(transTerm True
-                                          caslSign pcfolSign cfolSign globalVars
-                                                   fqTerm)
-                (transProcess' p)
+                -- Translate the term for use in the term prefix operator
+                cspProver_action_prefixOp (transCASLTerm' vsm TermPrefix fqTerm)
+                (transProcess' vsm p)
             InternalPrefixChoice v s _ ->
-                -- Use the nonfully qualified data instead of the fully
+                -- Use the non fully qualified data instead of the fully
                 -- qualified data as it is easier in this case as the variable
                 -- is not really a variable of that sort. Here the variable and
-                -- sort are seperate operands of the CSPProver operator.
+                -- sort are separate operands of the CSPProver operator.
                 cspProver_internal_prefix_choiceOp
-                (transVar v) (transSort s True) (transProcess' p)
+                (transVar v) (transSort NormalComm s)
+                                 (transProcess'
+                                  (Map.insert v PrefixChoice vsm) p)
             ExternalPrefixChoice v s _ ->
-                -- Use the nonfully qualified data instead of the fully
+                -- Use the non fully qualified data instead of the fully
                 -- qualified data as it is easier in this case as the variable
                 -- is not really a variable of that sort. Here the variable and
-                -- sort are seperate operands of the CSPProver operator.
+                -- sort are separate operands of the CSPProver operator.
                 cspProver_external_prefix_choiceOp
-                  (transVar v) (transSort s True)
-                                   (transProcess' p)
-            ChanSend _ _ _ -> conDouble "ChanSendNotYetDone"
+                  (transVar v) (transSort NormalComm s)
+                                   (transProcess'
+                                    (Map.insert v PrefixChoice vsm) p)
+            ChanSend _ _ _ ->
+                -- We do not use the non fully qualified term or channel name.
+                -- Instead we use the fully qualified term (fqTerm) and the
+                -- fully qualified channel (mfqc)
+                case mfqc of
+                  Nothing -> error "CspCASLProver.TransProcesses.transEvent: Missing fully qualified channel data"
+                  Just (chanName, chanSort) ->
+                      -- CspProver's channel send Op
+                      cspProver_chan_sendOp
+                      -- Name of channel
+                      (transChanName chanName)
+                      -- Term to send
+                      (transCASLTerm' vsm (ChanSendOrParam chanSort) fqTerm)
+                      -- The translated version of the rest of the process
+                      (transProcess' vsm p)
+
             ChanNonDetSend _ var varSort _ ->
                 -- We do not use the fully qualified variable (fqTerm) instead
@@ -179 +256 @@
                 case mfqc of
                   Nothing -> error "CspCASLProver.TransProcesses.transEvent: Missing fully qualified channel data"
-                  Just (chanName, chanSort) ->
-                      -- CspProvers channel non-deterministic channel send Op
-                      cspProver_chan_nondeterministic_sendOp
-                      -- The channel made of the name and the target sort of the
-                      -- channel
-                      (transChanName chanName chanSort)
-                      -- The translate variable
+                             -- Notice we do not use the derived channel's
+                             -- sort(second of Just) as this can be a sub type
+                             -- of the declared channel sort, which is what we
+                             -- need.
+                  Just (chanName, _) ->
+                      let declaredChanSort = case Map.lookup chanName chanMap of
+                                             Nothing -> error "CspCASLProver.TransProcesses.transEvent: Channel name not in channel map"
+                                             Just s -> s
+                      -- CspProvers non-deterministic channel send Op
+                      in cspProver_chan_nondeterministic_sendOp
+                      -- The channel name
+                      (transChanName chanName)
+                      -- The translated variable
                       (transVar var)
                       -- The translate sort (channel version) of the set to
-                      -- receive from
-                      (transSort varSort False)
+                      -- receive from. Note that the sort in the mfqc is the
+                      -- sort of the variable as specified, we want here the
+                      -- declaration sort of the channel.
+                      (transSort (ChanComm declaredChanSort) varSort)
                       -- The translated version of the rest of the process
-                      (transProcess' p)
-
-            ChanRecv _ _ _ _ -> conDouble "ChanRecvNotYetDone"
+                      (transProcess' (Map.insert var
+                                      (ChanSendOrRec declaredChanSort) vsm) p)
+
+            ChanRecv _ var varSort _ ->
+                -- We do not use the fully qualified variable (fqTerm) instead
+                -- we use the non fully qualified variable (var, varSort).
+                case mfqc of
+                  Nothing -> error "CspCASLProver.TransProcesses.transEvent: Missing fully qualified channel data"
+                  -- Notice we do not use the derived channel's sort(second of
+                  -- Just) as this can be a sub type of the declared channel
+                  -- sort, which is what we need.
+                  Just (chanName, _) ->
+                      let declaredChanSort = case Map.lookup chanName chanMap of
+                                             Nothing -> error "CspCASLProver.TransProcesses.transEvent: Channel name not in channel map"
+                                             Just s -> s
+                      -- CspProvers channel receive Op
+                      in cspProver_chan_recOp
+                      -- The channel name
+                      (transChanName chanName)
+                      -- The translated variable
+                      (transVar var)
+                      -- The translate sort (channel version) of the set to
+                      -- receive from. Note that the sort in the mfqc is the
+                      -- sort of the variable as specified, we want here the
+                      -- declaration sort of the channel.
+                      (transSort (ChanComm declaredChanSort) varSort)
+                      -- The translated version of the rest of the process
+                      (transProcess' (Map.insert var
+                                      (ChanSendOrRec declaredChanSort) vsm) p)
+
             FQEvent _ _ _ _ -> error "CspCASLProver.TransProcesses.transEvent: A FQEvent should not contain a non-FQEvent";
       _ ->  error "CspCASLProver.TransProcesses.transEvent: Expected a FQEvent not a non-FQEvent";
@@ -203 +315 @@
 transVar v = conDouble $ tokStr v
 
--- | Translate a sort into CspProver (Isabelle). If toFlat = true then the
---   result will be the corresponding flat type for a given sort else it will be
---   the data set type for the given sort i.e. toFlat = true for normal
---   communication, toFlat = false for channel communications
-transSort :: CASL_AS_Basic_CASL.SORT -> Bool -> Term
-transSort sort toFlat = if toFlat
-                        then conDouble $ mkSortFlatString sort
-                        else conDouble $ mkSortDataSetString sort
-
-transChanName :: CHANNEL_NAME -> CASL_AS_Basic_CASL.SORT -> Term
-transChanName chanName sort =
-    conDouble $ mkEventChannelConstructor chanName sort
-
-transRenaming :: RENAMING -> Term
-transRenaming _ = conDouble "RenamingNotDoneYet"
+-- | 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"
 
 -------------------------------------------------------------------------
@@ -225 +339 @@
 -- | 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 adding various functions around them depending
---   on if the variable is global or local.
-cspCaslTransRecord :: CASL_Sign.Sign f e -> FQProcVarList -> Set.Set String ->
+--   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 -> Record f Term Term
-cspCaslTransRecord caslSign globalVars tyToks trForm strs =
+                      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 translate the variable but wrap it in the
+     -- 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 r ->
+    { foldQual_var = \ _ v s _ ->
       let v' = mkFree $ CFOL2IsabelleHOL.transVar strs v
-      in -- If the variable is a global variable then add the
-         -- representation function before the choose function.
-        if ((CASL_AS_Basic_CASL.Qual_var v s r) `elem` globalVars)
-        then
-            -- Global variable
-            mkChooseFunOp s $ mkSortBarRepOp s $ v'
-        else
-            -- Local variable
-            mkChooseFunOp s $ 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 process term in to Isabelle HOL. The first parameter
---   decides if we should land in the alphabet or in a bar type. Both
---   of these are related by Abstraction and Representation fucntions
---   in Isabelle. The second parameter is he global variables of the
---   process. The third parameter is the data part (CASL signature)
---   for translating the translation of terms.
-transTerm :: Bool -> CASL_Sign.Sign () () -> CASL_Sign.Sign () () ->
-             CASL_Sign.Sign () () -> FQProcVarList ->
-             CASL_AS_Basic_CASL.TERM () -> Term
-transTerm toAlphabet  caslSign pcfolSign cfolSign globalVars caslTerm =
-    let strs = CFOL2IsabelleHOL.getAssumpsToks caslSign in
-    case caslTerm of
-      -- if the term is just a variable then we need to check if its
-      -- global and if we land in the alphabet or not. Each case has
-      -- different behaviour.
-      CASL_AS_Basic_CASL.Qual_var v s r ->
-          let v' = mkFree $ CFOL2IsabelleHOL.transVar strs v
-          in
-            -- Check if the variable is a global variabe
-            if ((CASL_AS_Basic_CASL.Qual_var v s r) `elem` globalVars)
-            then
-                -- Its a global Variable
-                -- Check if we are to land in the alphabet or now
-                if (toAlphabet)
-                then
-                    -- Land in the Alphabet
-                    (mkSortBarRepOp s) v'
-                else
-                    -- Land in the Bar Types
-                    v' -- Its already in the Bar Ype as its global
-            else
-                -- Its a local Variable
-                -- Check if we are to land in the alphabet or now
-                if (toAlphabet)
-                then
-                    -- Land in the Alphabet
-                    v' -- Its already in the alphabet as its local
-                else
-                    -- Land in the Bar Types
-                    (mkSortBarAbsOp s) v'
-
-      -- otherwise (not a variable) we add a classOp and constructor
-      -- around it and translate the arguments with the transCaslTermWithoutWrap
-      -- translator that adds a chooseOp, representation and
-      -- abstraction fucntiosn where needed.
-      _ -> 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 $
-                             transCaslTermWithoutWrap pcfolSign cfolSign
-                                                      globalVars caslTerm
-           in if (toAlphabet)
-              then isaCaslTerm
-              else (mkSortBarAbsOp sort) isaCaslTerm
+-- | 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 one exception, If we
---   are translating a variable then we must first add the correct choose
---   function around it to change it from an equivalence class to value of the
---   underlying sort. Also if we are translating a variable and the variable is
---   a global process variable then we must first apply Isabelle's
---   representation function to the variable. This function will always return a
---   term that is in the basic Sorts. i.e. to make it part of the alphabet it
---   will need to be wrapped up in a class operation with the necessary
---   constructor. We need the PCFOL and CFOL signature of the data part after
+--   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.
-transCaslTermWithoutWrap :: CASL_Sign.Sign () () -> CASL_Sign.Sign () () ->
-                            FQProcVarList -> CASL_AS_Basic_CASL.TERM () -> Term
-transCaslTermWithoutWrap pcfolSign cfolSign globalVars term =
-    let -- Function to remove subsorting - from comorphism CAS2PCFOL
+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 CAS2SubPCFOL
+        -- Function to remove partiality - from comorphism CASL2SubPCFOL
         -- This needs to match the translation CASL2SubCFOL.defaultCASL2SubCFOL
         b = True -- We want unique bottom elements per sort
@@ -335 +447 @@
         rmPartial = CASL_Simplify.simplifyTerm id .
                     CASL2SubCFOL.codeTerm b bsrts
-        -- Function to tranalate to Isabelle - from comorphism CFOL2IsabelleHOL
+        -- Function to translate to Isabelle - from comorphism CFOL2IsabelleHOL
         -- We need the CFOL signature to translate the terms properly
         tyToks = CFOL2IsabelleHOL.typeToks cfolSign
@@ -341 +453 @@
         strs = CFOL2IsabelleHOL.getAssumpsToks cfolSign
         toIsabelle = foldTerm $ cspCaslTransRecord cfolSign
-                     globalVars tyToks trForm strs
+                     tyToks trForm strs vsm
         --CFOL2IsabelleHOL.transFORMULA cfolSign tyToks trForm strs
     in toIsabelle $ rmPartial $ termNoSub
@@ -347 +459 @@
 -- | Translate a fully qualified CASL formula into an Isabelle Term using the
 --   exact translation as is done in the comorphism composition
---   CASL2PCFOL;defaultCASL2SubCFOL;CFOL2IsabelleHOL with one exception. The
---   exception is that a variable must have a choose function wrapped around it
---   and possible also a representation function (if it is a global
---   variable). We need the PCFOL and CFOL signature of the data part after
---   translation to CFOL to translate the formula.
-transFormula :: CASL_Sign.Sign () () -> CASL_Sign.Sign () () -> FQProcVarList ->
+--   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 globalVars formula =
+transFormula pcfolSign cfolSign vsm formula =
     let -- Function to remove subsorting - from comorphism CAS2PCFOL
         rmSub = CASL2PCFOL.f2Formula
@@ -369 +480 @@
                     CASL2SubCFOL.codeFormula b bsrts
         -- Function to tranalate to Isabelle - from comorphism CFOL2IsabelleHOL
-        -- We need the CFOL signature to translate the formulas properly
+        -- 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
-                     globalVars tyToks trForm strs
+                     tyToks trForm strs vsm
         --CFOL2IsabelleHOL.transFORMULA cfolSign tyToks trForm strs
     in toIsabelle $ rmPartial $ formulaNoSub

trunk/CspCASLProver/Utils.hs

@@ -21 +21 @@
     , addAllCompareWithFun
     , addAllIntegrationTheorems
-    , addDataSetTypes
     , addEqFun
     , addEventDataType
@@ -33 +32 @@
     ) where
 
-import CASL.AS_Basic_CASL (SORT, OpKind(..))
+import CASL.AS_Basic_CASL (SORT, OpKind(..), TERM(..))
 import qualified CASL.Fold as CASL_Fold
 import qualified CASL.Sign as CASLSign
@@ -48 +47 @@
 
 import CspCASL.AS_CspCASL_Process (PROCESS_NAME)
-import CspCASL.SignCSP (ChanNameMap, CspSign(..), ProcProfile(..),
-                        CspCASLSen(..), isProcessEq)
+import CspCASL.SignCSP (CspCASLSign, ccSig2CASLSign, ChanNameMap, CspSign(..),
+                        ProcProfile(..), CspCASLSen(..), isProcessEq)
 
 import CspCASLProver.Consts
 import CspCASLProver.IsabelleUtils
-import CspCASLProver.TransProcesses (transProcess)
+import CspCASLProver.TransProcesses (transProcess, VarSource(..))
 
 import qualified Data.List as List
@@ -134 +133 @@
                 lhs = termAppl lhs_a lhs_b
                 lhs_a = termAppl (conDouble funName) x
-                lhs_b = termAppl (conDouble (sort'Constructor)) y
+                lhs_b = termAppl (conDouble sort'Constructor) y
                 sort'SuperSet =CASLSign.supersortsOf sort' caslSign
                 commonSuperList = Set.toList (Set.intersection
@@ -142 +141 @@
                 -- If there are no tests then the rhs=false else
                 -- combine all tests using binConj
-                rhs = if (null allTests)
+                rhs = if null allTests
                       then false
                       else foldr1 binConj allTests
@@ -152 +151 @@
                 -- Test 4 =  test equality at: super sorts  vs super sorts
                 allTests = concat [test1, test2, test3, test4]
-                test1 = if (sort == sort') then [binEq x y] else []
+                test1 = if sort == sort' then [binEq x y] else []
                 test2 = if (Set.member sort sort'SuperSet)
                         then [binEq x (mkInjection sort' sort y)]
@@ -559 +558 @@
 
 -- | Add the Event datatype (built from a list of channels and the subsort
---  relation) to an Isabelle theory. BUG
+--  relation) to an Isabelle theory.
 addEventDataType :: Rel.Rel SORT -> ChanNameMap -> IsaTheory -> IsaTheory
 addEventDataType sortRel chanNameMap isaTh =
@@ -566 +565 @@
     in updateDomainTab eventDomainEntry isaTh
 
--- | Make a Domain Entry for the Event from a list of sorts. BUG
+-- | Make a Domain Entry for the Event from a list of sorts.
 mkEventDE :: Rel.Rel SORT -> ChanNameMap -> DomainEntry
-mkEventDE sortRel chanNameMap =
+mkEventDE _ chanNameMap =
     let flat = (mkVName flatS, [alphabetType])
-        -- Make a constuctor type pair for a channel with a target sort
-        mkCon (c, s) = (mkVName (mkEventChannelConstructor c s),
-                                 [mkSortBarType s])
-        -- Make pairs of channel and sorts, where the sorts are all the possible
-        -- predecessors of the sort of the channel.
-        mkChanSortPairs (cn,sort) =
-                -- get all predecessors including s
-            let subSorts = Set.insert sort (Rel.predecessors sortRel sort)
-                mkPair s = (cn,s)
-            in Set.toList $ Set.map mkPair subSorts
+        -- Make a constuctor type for a channel with a target sort
+        mkChanCon (c, s) = (mkVName (convertChannelString c),
+                                        [mkSortBarType s])
+        -- Make pairs of channel and sorts, where we only build the declared
+        -- channels and not the subsorted channels.
+        mkAllChanCons = map mkChanCon $ Map.toList chanNameMap
         -- We build the event type out of the flat constructions and the list of
         -- channel constructions
-    in (eventType, (flat:(map mkCon $ concat $ map mkChanSortPairs $
-                              Map.toList chanNameMap)))
+    in (eventType, (flat:mkAllChanCons))
 
 -- | Add the eq function to an Isabelle theory using a list of sorts
@@ -626 +620 @@
         sen = TypeDef flatType subset (IsaProof [] (By proof'))
         namedSen = (makeNamed sortFlatString sen)
-    in (isaTh_sign, isaTh_sen ++ [namedSen])
-
--- | Function to add all the Data Set types. These capture the original sorts by
---   creating sets of the bar varients. We use these sets when communicating
---   over a channel.
-addDataSetTypes :: [SORT] -> IsaTheory -> IsaTheory
-addDataSetTypes sorts isaTh = foldl addDataSetType isaTh sorts
-
--- | Function to add the Data Set type of a sort to an Isabelle theory.
-addDataSetType :: IsaTheory -> SORT -> IsaTheory
-addDataSetType isaTh sort =
-    let sortDataSetString = mkSortDataSetString sort
-        dataSetType = Type {typeId = sortDataSetString,
-                            typeSort = [],
-                            typeArgs =[]}
-        isaTh_sign = fst isaTh
-        isaTh_sen = snd isaTh
-        x = mkFree "x"
-        y = mkFree "y"
-        -- y in sort_Bar
-        condition1 = binMembership y (conDouble $ mkSortBarString sort)
-        -- x = Abs_sort_Bar y
-        condition2 = binEq x ((mkSortBarAbsOp sort) y)
-        -- y in x_Bar /\ x = Flat y
-        condition_eq = binConj condition1 condition2
-        exist_eq = termAppl (conDouble exS) (Abs y condition_eq NotCont)
-        subset = SubSet x (mkSortBarType sort) exist_eq
-        proof' = AutoSimpAdd Nothing [(mkSortBarString sort) ++ "_def"]
-        sen = TypeDef dataSetType subset (IsaProof [] (By proof'))
-        namedSen = (makeNamed sortDataSetString sen)
     in (isaTh_sign, isaTh_sen ++ [namedSen])
 
@@ -698 +662 @@
 --   signatures of the data part after translation to PCFOL and CFOL to pass
 --   along the process translation.
-addProcMap :: [Named CspCASLSen] -> CASLSign.Sign () () ->
+addProcMap :: [Named CspCASLSen] -> CspCASLSign ->
               CASLSign.Sign () () -> CASLSign.Sign () () ->
               IsaTheory -> IsaTheory
-addProcMap namedSens caslSign pcfolSign cfolSign isaTh =
-    let
+addProcMap namedSens ccSign pcfolSign cfolSign isaTh =
+    let caslSign = ccSig2CASLSign ccSign
         -- Translate a fully qualified variable (CASL term) to Isabelle
         tyToks = CFOL2IsabelleHOL.typeToks caslSign
@@ -729 +693 @@
                 varTerms = map transVar fqVars
                 lhs = procMapTerm (foldl termAppl (procNameTerm) varTerms)
-                rhs = transProcess caslSign pcfolSign cfolSign fqVars proc
+                addToVdm fqvar vdm' =
+                    case fqvar of
+                      Qual_var v _ _ -> Map.insert v GlobalParameter vdm'
+                      _ -> error "CspCASLProver.Utils.addProcMap: Term other than fully qualified variable in process parameter variable list"
+                vdm = foldr addToVdm Map.empty fqVars
+                rhs = transProcess ccSign pcfolSign cfolSign vdm proc
              in binEq lhs rhs
         -- to avoid warnings we specify the behaviour on CASL sentences. This

trunk/Isabelle/IsaConsts.hs

@@ -96 +96 @@
 membershipS :: String
 membershipS = "op :"
+
+-- | Imange of functions
+imageS :: String
+imageS = "image"
+
+rangeS :: String
+rangeS = "range"
 
 -- * some stuff for Isabelle
@@ -341 +348 @@
 -- * TERM CONSTRUCTORS
 -- | binary junctors
-binConj, binDisj, binImpl, binEqv, binEq, binEqvSim, binUnion, binMembership
+binConj, binDisj, binImpl, binEqv, binEq, binEqvSim, binUnion,
+       binMembership, binImageOp
     :: Term -> Term -> Term
 binConj = binVNameAppl conjV
@@ -351 +359 @@
 binUnion = binVNameAppl unionV
 binMembership = binVNameAppl membershipV
+binImageOp = binVNameAppl imageV
+
+rangeOp :: Term -> Term
+rangeOp t = termAppl (con rangeV) t
 
 -- | HOL function application
@@ -554 +566 @@
 membershipV :: VName
 membershipV = VName membershipS $ Just $ AltSyntax "(_ \\<in>/ _)" [65,66] 65
+
+imageV :: VName
+imageV = VName imageS $ Just $ AltSyntax "(_ `/ _)" [65,66] 65
+
+rangeV :: VName
+rangeV = VName rangeS Nothing
 
 -- **** keywords in theory files from the Isar Reference Manual 2005