Index: /trunk/Comorphisms/CFOL2IsabelleHOL.hs =================================================================== --- /trunk/Comorphisms/CFOL2IsabelleHOL.hs (revision 10903) +++ /trunk/Comorphisms/CFOL2IsabelleHOL.hs (revision 11215) @@ -20,7 +20,10 @@ , SignTranslator , FormulaTranslator + , getAssumpsToks + , formTrCASL , quantifyIsa , quantify , transSort + , transRecord , transOP_SYMB ) where Index: /trunk/Comorphisms/CASL2CspCASL.hs =================================================================== --- /trunk/Comorphisms/CASL2CspCASL.hs (revision 11201) +++ /trunk/Comorphisms/CASL2CspCASL.hs (revision 11215) @@ -26,5 +26,5 @@ -- CspCASL import CspCASL.Logic_CspCASL -import CspCASL.AS_CspCASL (CspBasicSpec (..), CspCASLSentence, emptyCCSentence) +import CspCASL.AS_CspCASL (CspBasicSpec (..)) import CspCASL.SignCSP @@ -41,5 +41,5 @@ Symbol RawSymbol ProofTree CspCASL () - CspBasicSpec CspCASLSentence SYMB_ITEMS SYMB_MAP_ITEMS + CspBasicSpec CspCASLSen SYMB_ITEMS SYMB_MAP_ITEMS CspCASLSign CspMorphism @@ -73,4 +73,4 @@ , pred_map = pred_map m } -mapSen :: CASLFORMULA -> CspCASLSentence -mapSen _ = emptyCCSentence +mapSen :: CASLFORMULA -> CspCASLSen +mapSen _ = emptyCCSen Index: /trunk/Comorphisms/CspCASL2Modal.hs =================================================================== --- /trunk/Comorphisms/CspCASL2Modal.hs (revision 11201) +++ /trunk/Comorphisms/CspCASL2Modal.hs (revision 11215) @@ -28,5 +28,5 @@ import CspCASL.Logic_CspCASL import CspCASL.SignCSP -import CspCASL.AS_CspCASL (CspBasicSpec (..), CspCASLSentence) +import CspCASL.AS_CspCASL (CspBasicSpec (..)) -- ModalCASL @@ -42,5 +42,5 @@ instance Comorphism CspCASL2Modal CspCASL () - CspBasicSpec CspCASLSentence SYMB_ITEMS SYMB_MAP_ITEMS + CspBasicSpec CspCASLSen SYMB_ITEMS SYMB_MAP_ITEMS CspCASLSign CspMorphism @@ -82,5 +82,5 @@ -mapSen :: CspCASLSentence -> ModalFORMULA +mapSen :: CspCASLSen -> ModalFORMULA mapSen _f = True_atom nullRange Index: /trunk/Comorphisms/CspCASL2IsabelleHOL.hs =================================================================== --- /trunk/Comorphisms/CspCASL2IsabelleHOL.hs (revision 10619) +++ /trunk/Comorphisms/CspCASL2IsabelleHOL.hs (revision 11215) @@ -27,4 +27,5 @@ import qualified Comorphisms.CFOL2IsabelleHOL as CFOL2IsabelleHOL import Comorphisms.CFOL2IsabelleHOL(IsaTheory) +import CspCASL.AS_CspCASL_Process (PROCESS_NAME) import CspCASL.Logic_CspCASL import CspCASL.AS_CspCASL @@ -49,5 +50,5 @@ instance Comorphism CspCASL2IsabelleHOL CspCASL () - CspBasicSpec CspCASLSentence SYMB_ITEMS SYMB_MAP_ITEMS + CspBasicSpec CspCASLSen SYMB_ITEMS SYMB_MAP_ITEMS CspCASLSign CspMorphism @@ -71,14 +72,17 @@ -- | Translate CspCASL theories to Isabelle -transCCTheory :: (CspCASLSign, [Named CspCASLSentence]) -> Result IsaTheory +transCCTheory :: (CspCASLSign, [Named CspCASLSen]) -> Result IsaTheory transCCTheory ccTheory = let ccSign = fst ccTheory ccSens = snd ccTheory + caslSign = ccSig2CASLSign ccSign + cspSign = ccSig2CspSign ccSign + casl2pcfol = (map_theory CASL2PCFOL.CASL2PCFOL) pcfol2cfol = (map_theory CASL2SubCFOL.defaultCASL2SubCFOL) cfol2isabelleHol = (map_theory CFOL2IsabelleHOL.CFOL2IsabelleHOL) sortList = Set.toList(CASLSign.sortSet caslSign) - --fakeType = Type {typeId = "Fake_Type" , typeSort = [], typeArgs =[]} + fakeType = Type {typeId = "Fake_Type" , typeSort = [], typeArgs =[]} in do -- Remove Subsorting from the CASL part of the CspCASL specification translation1 <- casl2pcfol (caslSign,[]) @@ -87,6 +91,7 @@ -- Next Translate to IsabelleHOL code translation3 <- cfol2isabelleHol translation2 - -- Next add the preAlpabet construction to the IsabelleHOL code - return $ addCspCaslSentences ccSens + -- Next add the preAlphabet construction to the IsabelleHOL code + return $ addProcMap ccSens caslSign + $ addProcNameDatatype cspSign $ addAllIntegrationTheorems sortList ccSign $ addAllChooseFunctions sortList @@ -99,33 +104,92 @@ $ addPreAlphabet sortList $ addWarning + -- hack: show the casl sentences + -- addConst (show(ccSens)) fakeType $ translation3 --- This is not implemented in a sensible way yet and is not used -transCCSentence :: CspCASLSign -> CspCASLSentence -> Result IsaSign.Sentence -transCCSentence _ (CspCASLSentence pn _ _) = +-- BUG This is not implemented in a sensible way yet and is not used +transCCSentence :: CspCASLSign -> CspCASLSen -> Result IsaSign.Sentence +transCCSentence _ (ProcessEq pn _ _ _) = do return (mkSen (Const (mkVName (show pn)) (Disp (Type "byeWorld" [] []) TFun Nothing))) --- | Add a list of CspCASL sentences to an Isabelle theory -addCspCaslSentences :: [Named CspCASLSentence] -> IsaTheory -> IsaTheory -addCspCaslSentences namedSens isaTh = - -- Create datatype for process names - -- crate constant - -- create primrec - -- create list of equations -- one for each sentence - foldl addCspCaslSentence isaTh namedSens - --- | Add a single CspCASL sentence to an Isabelle theory -addCspCaslSentence :: IsaTheory -> Named CspCASLSentence -> IsaTheory -addCspCaslSentence isaTh namedSen = - let sen = sentence namedSen - in case sen of - CspCASLSentence pn _ proc -> - let name = show pn - t1 = conDouble name - t2 = transProcess proc - in addDef name t1 t2 isaTh - --- Functions for adding the PreAlphabet datatype to an Isabelle theory +-------------------------------------------------------------------------- +-- Functions for adding the process name datatype to an Isabelle theory -- +-------------------------------------------------------------------------- + +-- | Add process name datatype which has a constructor for each +-- process name (along with the arguments for the process) in the +-- CspCASL Signature to an Isabelle theory +addProcNameDatatype :: CspSign -> IsaTheory -> IsaTheory +addProcNameDatatype cspSign isaTh = + let -- Create a list of pairs of process names and thier profiles + procSetList = Map.toList (procSet cspSign) + procNameDomainEntry = mkProcNameDE procSetList + in updateDomainTab procNameDomainEntry isaTh + + +-- | Make a proccess name Domain Entry from ... +mkProcNameDE :: [(PROCESS_NAME, ProcProfile)] -> DomainEntry +mkProcNameDE processes = + let -- The a list of pairs of constructors and their arguments + constructors = map mk_cons processes + -- Take a proccess name and its argument sorts (also its + -- commAlpha - thrown away) and make a pair representing the + -- constructor and the argument types + mk_cons (procName, (ProcProfile sorts _)) = + (mkVName (mkProcNameConstructor procName), map sortToTyp sorts) + -- Turn a sort in to a Typ suitable for the domain entry The + -- processes need to have arguments of the bar variants of + -- the sorts not the original sorts + sortToTyp sort = Type {typeId = mkSortBarString sort, + typeSort = [isaTerm], + typeArgs = []} + in + (procNameType, constructors) + +------------------------------------------------------------------------- +-- Functions adding the process map fucntion to an Isabelle theory -- +------------------------------------------------------------------------- + +-- | Add the fucction procMap to an Isabelle theory. This function +-- maps process names to real processes build using the same names +-- and the alphabet i.e., ProcName => (ProcName, Alphabet) proc. We +-- need to know the CspCASL sentences and the casl signature (data +-- part) +addProcMap :: [Named CspCASLSen] -> CASLSign.Sign () () -> IsaTheory -> + IsaTheory +addProcMap namedSens caslSign isaTh = + let + -- Build new Isabelle theory with additional constant + isaThWithConst = addConst procMapS procMapType isaTh + -- Get the plain sentences from the named senetences + sens = map (\namedsen -> sentence namedsen) namedSens + -- Filter so we only have proccess equations and no CASL senetences + processEqs = filter isProcessEq sens + -- the term representing the procMap that tajes a term as a + -- parameter + procMapTerm = termAppl (conDouble procMapS) + -- Make a single equation for the primrec from a process equation + -- BUG HERE - this next part is not right - underscore is bad + mkEq (ProcessEq procName vars _ proc) = + let -- Make the name (string) for this process + procNameString = convertProcessName2String procName + -- Change the name to a term + procNameTerm = conDouble procNameString + -- Turn the list of variables into a list of Isabelle + -- free variables + varTerms = [] -- BUG - should be somehting like map (\x -> mkFree (show x)) vars + -- Make a lhs term built of termAppl applied to the + -- proccess name and the variables + lhs = procMapTerm (foldl termAppl (procNameTerm) varTerms) + rhs = transProcess caslSign proc + in binEq lhs rhs + -- Build equations for primrec using process equations + eqs = map mkEq processEqs + in addPrimRec eqs isaThWithConst + +------------------------------------------------------------------------- +-- Functions for adding the PreAlphabet datatype to an Isabelle theory -- +------------------------------------------------------------------------- -- | Add the PreAlphabet (built from a list of sorts) to an Isabelle theory @@ -142,19 +206,18 @@ (mkVName (mkPreAlphabetConstructor sort), [Type {typeId = convertSort2String sort, - typeSort = [isaTerm], - typeArgs = []}]) + typeSort = [isaTerm], + typeArgs = []}]) ) sorts ) --- Functions for adding the eq functions and the compare_with --- functions to an Isabelle theory +---------------------------------------------------------------- +-- Functions for adding the eq functions and the compare_with -- +-- functions to an Isabelle theory -- +---------------------------------------------------------------- -- | Add the eq function to an Isabelle theory using a list of sorts addEqFun :: [SORT] -> IsaTheory -> IsaTheory addEqFun sortList isaTh = - let preAlphabetType = Type {typeId = preAlphabetS, - typeSort = [], - typeArgs =[]} - eqtype = mkFunType preAlphabetType $ mkFunType preAlphabetType boolType + let eqtype = mkFunType preAlphabetType $ mkFunType preAlphabetType boolType isaThWithConst = addConst eq_PreAlphabetS eqtype isaTh mkEq sort = @@ -183,7 +246,4 @@ addCompareWithFun ccSign isaTh sort = let sortList = Set.toList(CASLSign.sortSet ccSign) - preAlphabetType = Type {typeId = preAlphabetS, - typeSort = [], - typeArgs =[]} sortType = Type {typeId = convertSort2String sort, typeSort = [], typeArgs =[]} @@ -232,5 +292,7 @@ in addPrimRec eqs isaThWithConst --- Functions for producing the Justification theorems +-------------------------------------------------------- +-- Functions for producing the Justification theorems -- +-------------------------------------------------------- -- | Add all justification theorems to an Isabelle Theory. We need to @@ -409,4 +471,8 @@ in addThreomWithProof name thmConds thmConcl proof' isaTh +-------------------------------------------------------------- +-- Functions for producing instances of equivalence classes -- +-------------------------------------------------------------- + -- | Function to add preAlphabet as an equivalence relation to an -- Isabelle theory @@ -434,14 +500,12 @@ $ isaTh +------------------------------------------------------------- +-- Functions for producing the alphabet type and bar types -- +------------------------------------------------------------- + -- | Function to add the Alphabet type (type synonym) to an Isabelle theory addAlphabetType :: IsaTheory -> IsaTheory addAlphabetType isaTh = - let preAlphabetType = Type {typeId = preAlphabetS, - typeSort = [], - typeArgs =[]} - preAlphabetQuotType = Type {typeId = quotS, - typeSort = [], - typeArgs =[preAlphabetType]} - isaTh_sign = fst isaTh + let isaTh_sign = fst isaTh isaTh_sign_tsig = tsig isaTh_sign myabbrs = abbrs isaTh_sign_tsig @@ -460,9 +524,6 @@ addBarType :: IsaTheory -> SORT -> IsaTheory addBarType isaTh sort = - let sortBarString = convertSort2String sort ++ barExtS + let sortBarString = mkSortBarString sort barType = Type {typeId = sortBarString, typeSort = [], typeArgs =[]} - alphabetType = Type {typeId = alphabetS, - typeSort = [], - typeArgs =[]} isaTh_sign = fst isaTh isaTh_sen = snd isaTh @@ -538,5 +599,5 @@ Apply (SubgoalTac subgoalTacTerm), Apply(Simp), - Apply(Other ("unfold " ++ quotEqualityS)), + Apply(SimpAdd Nothing [quotEqualityS]), Apply(Other ("unfold "++ preAlphabetSimS ++ "_def")), @@ -544,4 +605,8 @@ Done in addThreomWithProof chooseFunName thmConds thmConcl proof' isaTh + +------------------------------------------------------ +-- Functions for producing the integration theorems -- +------------------------------------------------------ -- | Add all the integration theorems. We need to know all the sorts @@ -573,5 +638,6 @@ then false else - -- pick any common sort - we should pick the top most one. + -- BUG pick any common sort for now (this does hold + -- and is valid) we should pick the top most one. let s' = head commonSuperList in binEq (mkInjection s1 s' x) (mkInjection s2 s' y) @@ -589,6 +655,10 @@ in addThreomWithProof "IntegrationTheorem_A" thmConds thmConcl proof' isaTh --- Function to help keep strings consistent - +---------------------------------------------- +-- Function to help keep strings consistent -- +---------------------------------------------- + +-- | String of the name of the function to compare eqaulity of two +-- elements of the PreAlphabet eq_PreAlphabetS :: String eq_PreAlphabetS = "eq_PreAlphabet" @@ -603,10 +673,4 @@ quotEqualityS :: String quotEqualityS = "quot_equality" - -preAlphabetS :: String -preAlphabetS = "PreAlphabet" - -quotS :: String -quotS = "quot" reflexivityTheoremS :: String @@ -769,5 +833,8 @@ -- Function that returns the constructor of PreAlphabet for a given sort mkPreAlphabetConstructor :: SORT -> String -mkPreAlphabetConstructor sort = "C_" ++ (show sort) +mkPreAlphabetConstructor sort = "C_" ++ (convertSort2String sort) + +mkProcNameConstructor :: PROCESS_NAME -> String +mkProcNameConstructor pn = show pn -- Function that takes a sort and outputs a the function name for the @@ -781,5 +848,13 @@ mkChooseFunName sort = ("choose_" ++ (mkPreAlphabetConstructor sort)) --- Functions for manipulating an Isabelle theory + + +-- Converts a SORT in to the corresponding bar sort represented as a +-- string +mkSortBarString :: SORT -> String +mkSortBarString s = convertSort2String s ++ barExtS +--------------------------------------------------- +-- Functions for manipulating an Isabelle theory -- +--------------------------------------------------- -- Add a single constant to the signature of an Isabelle theory @@ -845,5 +920,7 @@ in (isaTh_sign, isaTh_sen ++ [namedSen]) --- Code below this line is junk +---------------------------------- +-- Code below this line is junk -- +---------------------------------- -- Add a warning to an Isabelle theory Index: /trunk/CspCASL/SignCSP.hs =================================================================== --- /trunk/CspCASL/SignCSP.hs (revision 10827) +++ /trunk/CspCASL/SignCSP.hs (revision 11215) @@ -17,13 +17,20 @@ module CspCASL.SignCSP where -import CspCASL.AS_CspCASL_Process (CHANNEL_NAME, PROCESS_NAME) - -import CASL.AS_Basic_CASL (SORT) +import CspCASL.AS_CspCASL_Process (CHANNEL_NAME, PROCESS_NAME, + PROCESS(..), CommAlpha(..), CommType(..), TypedChanName(..)) + +import CspCASL.AS_CspCASL () +import CspCASL.Print_CspCASL + +import CASL.AS_Basic_CASL (FORMULA, SORT) import CASL.Sign (emptySign, Sign, extendedInfo, sortRel) import CASL.Morphism (Morphism) -import qualified Common.Doc as Doc -import qualified Common.DocUtils as DocUtils -import Common.Id (Id, SIMPLE_ID) +import Common.AS_Annotation (Named) + +import Common.Doc +import Common.DocUtils + +import Common.Id (Id, SIMPLE_ID, mkSimpleId, nullRange) import Common.Lib.Rel (predecessors) import Common.Result @@ -38,20 +45,8 @@ deriving (Eq, Show) --- | A process communication alphabet consists of a set of sort names --- and typed channel names. -data TypedChanName = TypedChanName CHANNEL_NAME SORT - deriving (Eq, Ord, Show) -data CommType = CommTypeSort SORT - | CommTypeChan TypedChanName - deriving (Eq, Ord) -instance Show CommType where - show (CommTypeSort s) = show s - show (CommTypeChan (TypedChanName c s)) = show (c, s) - -type CommAlpha = Set.Set CommType - type ChanNameMap = Map.Map CHANNEL_NAME SORT type ProcNameMap = Map.Map PROCESS_NAME ProcProfile type ProcVarMap = Map.Map SIMPLE_ID SORT +type ProcVarList = [(SIMPLE_ID, SORT)] -- Close a communication alphabet under CASL subsort @@ -99,4 +94,7 @@ { chans :: ChanNameMap , procSet :: ProcNameMap + -- | Added for uniformity to the CASL static analysis. After + -- static analysis this is the empty list. + , ccSentences :: [Named CspCASLSen] } deriving (Eq, Show) @@ -107,4 +105,7 @@ ccSig2CASLSign :: CspCASLSign -> Sign () () ccSig2CASLSign sigma = sigma { extendedInfo = () } + +ccSig2CspSign :: CspCASLSign -> CspSign +ccSig2CspSign sigma = extendedInfo sigma -- | Empty CspCASL signature. @@ -117,4 +118,5 @@ { chans = Map.empty , procSet = Map.empty + , ccSentences =[] } @@ -170,6 +172,43 @@ -- dummy instances, need to be elaborated! -instance DocUtils.Pretty CspSign where - pretty = Doc.text . show -instance DocUtils.Pretty CspAddMorphism where - pretty = Doc.text . show +instance Pretty CspSign where + pretty = text . show +instance Pretty CspAddMorphism where + pretty = text . show + +-- Sentences + +-- A CspCASl senetence is either a CASL formula or a Procsses +-- equation. A process equation has on the LHS a process name, a list +-- of parameters which are qualified variables (which are terms), a +-- constituent communication alphabet and finally on the RHS a fully +-- qualified process. +data CspCASLSen = CASLSen (FORMULA ()) + | ProcessEq PROCESS_NAME ProcVarList CommAlpha PROCESS + deriving (Show, Eq, Ord) + +instance Pretty CspCASLSen where + -- Not implemented yet - the pretty printing of the casl sentences + pretty(CASLSen _) = text "Pretty printing for CASLSen not implemented yet" + pretty(ProcessEq pn varList alpha proc) = + let varDoc = if (null varList) + then empty + else parens $ sepByCommas $ map pretty (map fst varList) + in pretty pn <+> varDoc <+> equals <+> pretty proc + +emptyCCSen :: CspCASLSen +emptyCCSen = + let emptyProcName = mkSimpleId "empty" + emptyVarList = [] + emptyAlphabet = Set.empty + emptyProc = Skip nullRange + in ProcessEq emptyProcName emptyVarList emptyAlphabet emptyProc + +isCASLSen :: CspCASLSen -> Bool +isCASLSen (CASLSen _) = True +isCASLSen _ = False + +isProcessEq :: CspCASLSen -> Bool +isProcessEq (ProcessEq _ _ _ _) = True +isProcessEq _ = False + Index: /trunk/CspCASL/Trans_Consts.hs =================================================================== --- /trunk/CspCASL/Trans_Consts.hs (revision 10619) +++ /trunk/CspCASL/Trans_Consts.hs (revision 11215) @@ -19,12 +19,72 @@ import CASL.AS_Basic_CASL +import CspCASL.AS_CspCASL_Process (PROCESS_NAME) import Isabelle.IsaConsts import Isabelle.IsaSign +import Isabelle.Translate(showIsaTypeT) +-- Name for the PreAlphabet +preAlphabetS :: String +preAlphabetS = "PreAlphabet" + +-- Type for the PreAlphabet +preAlphabetType :: Typ +preAlphabetType = Type {typeId = preAlphabetS, + typeSort = [], + typeArgs =[]} + +-- Name for the Alphabet alphabetS :: String alphabetS = "Alphabet" +-- Type for the Alphabet +alphabetType :: Typ +alphabetType = Type {typeId = alphabetS, + typeSort = [], + typeArgs =[]} + +-- Name for IsabelleHOL quot type +quotS :: String +quotS = "quot" + +-- Type for preAlphabet quot +preAlphabetQuotType :: Typ +preAlphabetQuotType = Type {typeId = quotS, + typeSort = [], + typeArgs =[preAlphabetType]} + +-- Name for the datatype of process names +procNameS :: String +procNameS = "ProcName" + +-- Type for the datatype of process names +procNameType :: Typ +procNameType = Type {typeId = procNameS, + typeSort = [], + typeArgs =[]} + +-- name for CspProvers ('pn, 'a) proc type +procS :: String +procS = "proc" + +-- Type for (ProcName,Alpahbet) proc +cCProverProcType :: Typ +cCProverProcType = Type {typeId = procS, + typeSort = [], + typeArgs =[procNameType, alphabetType]} + +-- Name for the function for mapping process names to real processes +procMapS :: String +procMapS = "ProcMap" + +-- Type for the function for mapping process names to real processes +procMapType :: Typ +procMapType = mkFunType procNameType cCProverProcType + barExtS :: String barExtS = "_Bar" + +baseSign :: BaseSig +baseSign = Main_thy classS :: String @@ -36,3 +96,6 @@ -- Convert a SORT to a string convertSort2String :: SORT -> String -convertSort2String s = show s +convertSort2String s = showIsaTypeT s baseSign + +convertProcessName2String :: PROCESS_NAME -> String +convertProcessName2String pn = (show pn) Index: /trunk/CspCASL/AS_CspCASL_Process.der.hs =================================================================== --- /trunk/CspCASL/AS_CspCASL_Process.der.hs (revision 10428) +++ /trunk/CspCASL/AS_CspCASL_Process.der.hs (revision 11215) @@ -21,8 +21,12 @@ PROCESS_NAME, RENAMING, + CommAlpha(..), + CommType(..), + TypedChanName(..) ) where import CASL.AS_Basic_CASL (FORMULA, SORT, TERM, VAR) import Common.Id +import qualified Data.Set as Set -- DrIFT command @@ -47,5 +51,4 @@ type RENAMING = [Id] - type CHANNEL_NAME = SIMPLE_ID @@ -54,4 +57,18 @@ type COMM_TYPE = SIMPLE_ID +-- | A process communication alphabet consists of a set of sort names +-- and typed channel names. +data TypedChanName = TypedChanName CHANNEL_NAME SORT + deriving (Eq, Ord, Show) + +data CommType = CommTypeSort SORT + | CommTypeChan TypedChanName + deriving (Eq, Ord) + +instance Show CommType where + show (CommTypeSort s) = show s + show (CommTypeChan (TypedChanName c s)) = show (c, s) + +type CommAlpha = Set.Set CommType -- |CSP-CASL process expressions. @@ -96,3 +113,6 @@ -- | Named process | NamedProcess PROCESS_NAME [TERM ()] Range + -- | Fully qualified process. The range here shall be the same as + -- | in the process. + | FQProcess PROCESS CommAlpha Range deriving (Eq, Ord, Show) Index: /trunk/CspCASL/AS_CspCASL.der.hs =================================================================== --- /trunk/CspCASL/AS_CspCASL.der.hs (revision 10471) +++ /trunk/CspCASL/AS_CspCASL.der.hs (revision 11215) @@ -14,12 +14,12 @@ module CspCASL.AS_CspCASL where +import Common.Doc +import Common.DocUtils import Common.Id -import CASL.AS_Basic_CASL (SORT, VAR) +import CASL.AS_Basic_CASL (SORT, VAR, FORMULA) import CspCASL.AS_CspCASL_Process (CHANNEL_NAME, COMM_TYPE, PROCESS(..), PROCESS_NAME) - -import Common.Id -- DrIFT command @@ -34,4 +34,7 @@ deriving Show +data PROC_ALPHABET = ProcAlphabet [COMM_TYPE] Range + deriving (Show,Ord, Eq) + data PROC_ITEM = Proc_Decl PROCESS_NAME PROC_ARGS PROC_ALPHABET | Proc_Eq PARM_PROCNAME PROCESS @@ -42,17 +45,2 @@ data PARM_PROCNAME = ParmProcname PROCESS_NAME [VAR] deriving Show - -data PROC_ALPHABET = ProcAlphabet [COMM_TYPE] Range - deriving Show - --- Sentences - -data CspCASLSentence = CspCASLSentence PROCESS_NAME [VAR] PROCESS - deriving (Show, Eq, Ord) - -emptyProcName :: PROCESS_NAME -emptyProcName = mkSimpleId "empty" - -emptyCCSentence :: CspCASLSentence -emptyCCSentence = CspCASLSentence emptyProcName [] - (NamedProcess emptyProcName [] nullRange) Index: /trunk/CspCASL/Trans_CspProver.hs =================================================================== --- /trunk/CspCASL/Trans_CspProver.hs (revision 10931) +++ /trunk/CspCASL/Trans_CspProver.hs (revision 11215) @@ -15,7 +15,11 @@ module CspCASL.Trans_CspProver where -import CASL.AS_Basic_CASL (SORT, VAR) +import qualified CASL.AS_Basic_CASL as CASL_AS_Basic_CASL +import qualified CASL.Fold as CASL_Fold +import qualified CASL.Sign as CASL_Sign import Common.Id + +import qualified Comorphisms.CFOL2IsabelleHOL as CFOL2IsabelleHOL import CspCASL.AS_CspCASL_Process @@ -26,6 +30,6 @@ import Isabelle.IsaConsts -transProcess :: PROCESS -> Term -transProcess pr = case pr of +transProcess :: CASL_Sign.Sign () () -> PROCESS -> Term +transProcess caslSign pr = case pr of -- precedence 0 Skip _ -> cspProver_skipOp @@ -41,43 +45,52 @@ -- precedence 1 ConditionalProcess _ p q _ -> - cspProver_conditionalOp true (transProcess p) (transProcess q) + cspProver_conditionalOp true (transProcess caslSign p) + (transProcess caslSign q) -- precedence 2 Hiding p es _ -> - cspProver_hidingOp (transProcess p) (transEventSet es) + cspProver_hidingOp (transProcess caslSign p) (transEventSet es) RenamingProcess p r _ -> - cspProver_renamingOp (transProcess p) (transRenaming r) + cspProver_renamingOp (transProcess caslSign p) (transRenaming r) -- precedence 3 Sequential p q _ -> - cspProver_sequenceOp (transProcess p) (transProcess q) + cspProver_sequenceOp (transProcess caslSign p) (transProcess caslSign q) PrefixProcess ev p _ -> - cspProver_action_prefixOp (transEvent ev) (transProcess p) + cspProver_action_prefixOp (transEvent caslSign ev) + (transProcess caslSign p) InternalPrefixProcess v s p _ -> cspProver_internal_prefix_choiceOp (transVar v) (transSort s) - (transProcess p) + (transProcess caslSign p) ExternalPrefixProcess v s p _ -> cspProver_external_prefix_choiceOp (transVar v) (transSort s) - (transProcess p) + (transProcess caslSign p) -- precedence 4 InternalChoice p q _ -> - cspProver_internal_choiceOp (transProcess p) (transProcess q) + cspProver_internal_choiceOp (transProcess caslSign p) + (transProcess caslSign q) ExternalChoice p q _ -> - cspProver_external_choiceOp (transProcess p) (transProcess q) + cspProver_external_choiceOp (transProcess caslSign p) + (transProcess caslSign q) -- precedence 5 Interleaving p q _ -> - cspProver_interleavingOp (transProcess p) (transProcess q) + cspProver_interleavingOp (transProcess caslSign p) + (transProcess caslSign q) SynchronousParallel p q _ -> - cspProver_synchronousOp (transProcess p) (transProcess q) + cspProver_synchronousOp (transProcess caslSign p) + (transProcess caslSign q) GeneralisedParallel p es q _ -> - cspProver_general_parallelOp (transProcess p) + cspProver_general_parallelOp (transProcess caslSign p) (transEventSet es) - (transProcess q) + (transProcess caslSign q) AlphabetisedParallel p les res q _ -> - cspProver_alphabetised_parallelOp (transProcess p) + cspProver_alphabetised_parallelOp (transProcess caslSign p) (transEventSet les) (transEventSet res) - (transProcess q) + (transProcess caslSign q) + -- BUG not done right yet + FQProcess p _ _ -> + transProcess caslSign p transEventSet :: EVENT_SET -> Term @@ -88,16 +101,16 @@ EventSet commTypes _ -> Set $ FixedSet $ map tranCommType commTypes -transEvent :: EVENT -> Term -transEvent ev = +transEvent :: CASL_Sign.Sign () () -> EVENT -> Term +transEvent caslSign ev = case ev of - TermEvent _caslTerm _ -> conDouble "not yet done" - ChanSend _ _ _ -> conDouble "not yet done" - ChanNonDetSend _ _ _ _ -> conDouble "not yet done" - ChanRecv _ _ _ _ -> conDouble "not yet done" + TermEvent caslTerm _ -> transTerm_with_class caslSign caslTerm + ChanSend _ _ _ -> conDouble "ChanSendNotYetDone" + ChanNonDetSend _ _ _ _ -> conDouble "ChanNonDetSendNotYetDone" + ChanRecv _ _ _ _ -> conDouble "ChanRecvNotYetDone" -transVar :: VAR -> Term +transVar :: CASL_AS_Basic_CASL.VAR -> Term transVar v = conDouble $ tokStr v -transSort :: SORT -> Term +transSort :: CASL_AS_Basic_CASL.SORT -> Term transSort sort = let sortBarString = convertSort2String sort ++ barExtS in conDouble sortBarString @@ -105,2 +118,68 @@ transRenaming :: RENAMING -> Term transRenaming _ = conDouble "not yet done" + + + +-- BUG - I dont think these functions are correct +transTerm_with_class :: CASL_Sign.Sign () () -> CASL_AS_Basic_CASL.TERM () -> + Term +transTerm_with_class caslSign caslTerm = + case caslTerm of + -- if the term is just a variable then we just translate the + -- variable to isabelle + CASL_AS_Basic_CASL.Qual_var _ _ _ -> transCaslTerm caslSign caslTerm + -- otherwise we add a classOp around it and translate the inside of + -- it with the translator that adds a chooseOp + _ -> classOp (transTerm_with_choose caslSign caslTerm) + +transTerm_with_choose :: CASL_Sign.Sign () () -> CASL_AS_Basic_CASL.TERM () -> + Term +transTerm_with_choose caslSign caslTerm = + case caslTerm of + -- if the term is just a variable then we need to apply the choose + -- function + CASL_AS_Basic_CASL.Qual_var _ _ _ -> termAppl (conDouble "choose") + (transCaslTerm caslSign caslTerm) + -- otherwise we just translate it to Isabelle + _ -> transCaslTerm caslSign caslTerm + +-- | Translate a CASL Term to an Isabelle Term using the exact +-- translation as is done in the comorphism composition +-- CASL2PCFOL;defaultCASL2SubCFOL;CFOL2IsabelleHOL +transCaslTerm :: CASL_Sign.Sign () () -> CASL_AS_Basic_CASL.TERM () -> Term +transCaslTerm caslSign caslTerm = + let tyToks = CFOL2IsabelleHOL.typeToks caslSign + trForm = CFOL2IsabelleHOL.formTrCASL + strs = CFOL2IsabelleHOL.getAssumpsToks caslSign + in CASL_Fold.foldTerm (CFOL2IsabelleHOL.transRecord + caslSign tyToks trForm strs) caslTerm + + +-- My own version of transRecord +-- transRecord_Term :: CASL.Sign.Sign f e -> Set.Set String -> FormulaTranslator f e +-- -> Set.Set String -> Record f Term Term +-- transRecord_Term sign tyToks tr toks = Record +-- { foldSimpleId = error "transRecord_Term: Simple_id" +-- , foldQual_var = \ _ v _ _ -> mkFree $ transVar toks v +-- , foldApplication = \ _ opsymb args _ -> +-- foldl termAppl (con $ transOP_SYMB sign tyToks opsymb) args +-- , foldSorted_term = \ _ t _ _ -> t -- no subsorting assumed +-- , foldCast = \ _ t _ _ -> t -- no subsorting assumed +-- , foldConditional = \ _ t1 phi t2 _ -> -- equal types assumed +-- If phi t1 t2 NotCont +-- , foldMixfix_qual_pred = error "transRecord_Term: Mixfix_qual_pred" +-- , foldMixfix_term = error "transRecord_Term: Mixfix_term" +-- , foldMixfix_token = error "transRecord_Term: Mixfix_token" +-- , foldMixfix_sorted_term = error "transRecord_Term: Mixfix_sorted_term" +-- , foldMixfix_cast = error "transRecord_Term: Mixfix_cast" +-- , foldMixfix_parenthesized = error "transRecord_Term: Mixfix_parenthesized" +-- , foldMixfix_bracketed = error "transRecord_Term: Mixfix_bracketed" +-- , foldMixfix_braced = error "transRecord_Term: Mixfix_braced" +-- } + +-- transVar :: Set.Set String -> VAR -> String +-- transVar toks v = let +-- s = showIsaConstT (simpleIdToId v) baseSign +-- renVar t = if Set.member t toks then renVar $ "X_" ++ t else t +-- in renVar s + Index: /trunk/CspCASL/StatAnaCSP.hs =================================================================== --- /trunk/CspCASL/StatAnaCSP.hs (revision 11201) +++ /trunk/CspCASL/StatAnaCSP.hs (revision 11215) @@ -21,5 +21,7 @@ import qualified Data.Maybe as Maybe import qualified Data.Set as S - +-- liam added the following, they should be deleted from imports when +-- liams temp code is removed: Op_name mkSimpleId mkInfix OP_SYMB(..), +-- OP_TYPE(..) import CASL.AS_Basic_CASL (FORMULA(..), OpKind(..), SORT, TERM(..), VAR, VAR_DECL(..)) @@ -34,5 +36,5 @@ import Common.ConvertGlobalAnnos import qualified Common.Lib.Rel as Rel -import Common.Id (getRange, Id, simpleIdToId, nullRange, mkSimpleId) +import Common.Id (getRange, Id, simpleIdToId, nullRange) import Common.Lib.State import Common.ExtSign @@ -44,8 +46,10 @@ import CspCASL.SignCSP +import qualified Data.Set as Set + basicAnalysisCspCASL :: (CspBasicSpec, CspCASLSign, GlobalAnnos) -> Result (CspBasicSpec, ExtSign CspCASLSign (), - [Named CspCASLSentence]) -basicAnalysisCspCASL (cc, sigma, ga) = do + [Named CspCASLSen]) +basicAnalysisCspCASL (cc, sigma, ga) = let Result es mga = mergeGlobalAnnos ga $ globAnnos sigma (_, accSig) = runState (ana_BASIC_CSP cc) $ case mga of @@ -53,24 +57,12 @@ Just nga -> sigma { globAnnos = nga } ds = reverse $ envDiags accSig - Result (es ++ ds) (Just ()) -- insert diagnostics - return (cc, mkExtSign accSig, [makeNamed "empty_sentence" emptyCCSentence, - makeNamed "StopProcSen" stopProc, - makeNamed "GParProcSen" gParProc, - makeNamed "AParProcSen" aParProc, - makeNamed "StopProcSen" seqProc]) - where - stopProc = CspCASLSentence (mkSimpleId "stopProc") [] (Stop nullRange) - seqProc = CspCASLSentence (mkSimpleId "seqProc") [] - (Sequential (Stop nullRange) - (Stop nullRange) nullRange) - gParProc = CspCASLSentence (mkSimpleId "gParProc") [] - (GeneralisedParallel (Stop nullRange) - (EventSet [mkSimpleId "S"] nullRange) - (Skip nullRange) nullRange) - aParProc = CspCASLSentence (mkSimpleId "gParProc") [] - (AlphabetisedParallel (Stop nullRange) - (EventSet [mkSimpleId "T"] nullRange) - (EventSet [mkSimpleId "U"] nullRange) - (Skip nullRange) nullRange) + -- Extract process equations only. + ext = extendedInfo accSig + ccsents = reverse $ ccSentences ext + -- Clean signature here + cleanSig = accSig + { extendedInfo = ext { ccSentences = []}} + in Result (es ++ ds) $ + Just (cc, mkExtSign cleanSig, ccsents) ana_BASIC_CSP :: CspBasicSpec -> State CspCASLSign () @@ -102,5 +94,5 @@ -- | Statically analyse a CspCASL channel declaration. -anaChanDecl :: CHANNEL_DECL -> State CspCASLSign CHANNEL_DECL +anaChanDecl :: CHANNEL_DECL -> State CspCASLSign () anaChanDecl (ChannelDecl chanNames chanSort) = do checkSorts [chanSort] -- check channel sort is known @@ -113,5 +105,5 @@ , envDiags = vds } - return (ChannelDecl chanNames chanSort) + return () -- | Statically analyse a CspCASL channel name. @@ -178,142 +170,181 @@ sig <- get let ext = extendedInfo sig + ccsens = ccSentences ext procDecls = procSet ext prof = pn `Map.lookup` procDecls case prof of - -- Only analyse a process if its name (and thus profile) is known - Just (ProcProfile procArgs procAlpha) -> - do gVars <- anaProcVars pn procArgs vs -- compute global vars - termAlpha <- anaProcTerm proc gVars Map.empty - checkCommAlphaSub termAlpha procAlpha proc "process equation" - return () - Nothing -> - do addDiags [mkDiag Error "process equation for unknown process" pn] - return () - vds <- gets envDiags - put sig { envDiags = vds } + -- Only analyse a process if its name (and thus profile) is known + Just (ProcProfile procArgs procAlpha) -> + do gVars <- anaProcVars pn procArgs vs -- compute global vars + (termAlpha, fqProc) <- anaProcTerm proc (Map.fromList gVars) Map.empty + checkCommAlphaSub termAlpha procAlpha proc "process equation" + -- Save the diags from the checkCommAlphaSub + vds <- gets envDiags + -- put CspCASL Sentences back in to the state with new sentence + put sig {envDiags = vds, extendedInfo = + ext { ccSentences = + -- BUG - What should the constituent + -- alphabet be for this process? + -- probably the same as the inner one! + (makeNamed ("ProcHugo") + (ProcessEq pn gVars + Set.empty + fqProc)):ccsens + } + } + return () + Nothing -> + do addDiags [mkDiag Error "process equation for unknown process" pn] + return () return () -- | Statically analyse a CspCASL process equation's global variable -- names. -anaProcVars :: PROCESS_NAME -> [SORT] -> [VAR] -> State CspCASLSign ProcVarMap +anaProcVars :: PROCESS_NAME -> [SORT] -> [VAR] -> State CspCASLSign ProcVarList anaProcVars pn ss vs = do case (compare (length ss) (length vs)) of LT -> do addDiags [mkDiag Error "too many process arguments" pn] - return Map.empty + return [] GT -> do addDiags [mkDiag Error "not enough process arguments" pn] - return Map.empty - EQ -> Monad.foldM anaProcVar Map.empty (zip vs ss) + return [] + EQ -> Monad.foldM anaProcVar [] (zip vs ss) -- | Statically analyse a CspCASL process-global variable name. -anaProcVar :: ProcVarMap -> (VAR, SORT) -> State CspCASLSign ProcVarMap +anaProcVar :: ProcVarList -> (VAR, SORT) -> State CspCASLSign ProcVarList anaProcVar old (v, s) = do - if v `Map.member` old - then do addDiags [mkDiag Error "process arg declared more than once" v] + if v `elem` (map fst old) + then do addDiags [mkDiag Error "process argument declared more than once" v] return old - else return (Map.insert v s old) + else return (old ++ [(v, s)]) -- Static analysis of process terms +-- BUG in fucntion below +-- not returing FQProcesses -- | Statically analyse a CspCASL process term. +-- The process that is returned is a fully qualified process. anaProcTerm :: PROCESS -> ProcVarMap -> ProcVarMap -> - State CspCASLSign CommAlpha + State CspCASLSign (CommAlpha, PROCESS) anaProcTerm proc gVars lVars = case proc of - NamedProcess name args _ -> + NamedProcess name args range -> do addDiags [mkDiag Debug "Named process" proc] al <- anaNamedProc proc name args (lVars `Map.union` gVars) - return al - Skip _ -> + return (al, + FQProcess (NamedProcess name args range) al range) + Skip range -> do addDiags [mkDiag Debug "Skip" proc] - return S.empty - Stop _ -> + return (S.empty, + FQProcess (Skip range) S.empty range) + Stop range -> do addDiags [mkDiag Debug "Stop" proc] - return S.empty - Div _ -> + return (S.empty, + FQProcess (Stop range) S.empty range) + Div range -> do addDiags [mkDiag Debug "Div" proc] - return S.empty - Run es _ -> + return (S.empty, + FQProcess (Div range) S.empty range) + Run es range -> do addDiags [mkDiag Debug "Run" proc] comms <- anaEventSet es - return comms - Chaos es _ -> + return (comms, + FQProcess (Run es range) comms range) + Chaos es range -> do addDiags [mkDiag Debug "Chaos" proc] comms <- anaEventSet es - return comms - PrefixProcess e p _ -> + return (comms, + FQProcess (Chaos es range) comms range) + PrefixProcess e p range -> do addDiags [mkDiag Debug "Prefix" proc] (evComms, rcvMap) <- anaEvent e (lVars `Map.union` gVars) - comms <- anaProcTerm p gVars (rcvMap `Map.union` lVars) - return (comms `S.union` evComms) - InternalPrefixProcess v s p _ -> + (comms, pFQTerm) <- anaProcTerm p gVars (rcvMap `Map.union` lVars) + return (comms `S.union` evComms, + FQProcess (PrefixProcess e pFQTerm range) (comms `S.union` evComms) range) + InternalPrefixProcess v s p range -> do addDiags [mkDiag Debug "Internal prefix" proc] checkSorts [s] -- check sort is known - comms <- anaProcTerm p gVars (Map.insert v s lVars) - return (S.insert (CommTypeSort s) comms) - ExternalPrefixProcess v s p _ -> + (comms, pFQTerm) <- anaProcTerm p gVars (Map.insert v s lVars) + return (S.insert (CommTypeSort s) comms, + FQProcess (InternalPrefixProcess v s pFQTerm range) (S.insert (CommTypeSort s) comms) range) + ExternalPrefixProcess v s p range -> do addDiags [mkDiag Debug "External prefix" proc] checkSorts [s] -- check sort is known - comms <- anaProcTerm p gVars (Map.insert v s lVars) - return (S.insert (CommTypeSort s) comms) - Sequential p q _ -> + (comms, pFQTerm) <- anaProcTerm p gVars (Map.insert v s lVars) + return (S.insert (CommTypeSort s) comms, + FQProcess (ExternalPrefixProcess v s pFQTerm range) (S.insert (CommTypeSort s) comms) range) + Sequential p q range -> do addDiags [mkDiag Debug "Sequential" proc] - pComms <- anaProcTerm p gVars lVars - qComms <- anaProcTerm q gVars Map.empty - return (pComms `S.union` qComms) - InternalChoice p q _ -> + (pComms, pFQTerm) <- anaProcTerm p gVars lVars + (qComms, qFQTerm) <- anaProcTerm q gVars Map.empty + return (pComms `S.union` qComms, + FQProcess (Sequential pFQTerm qFQTerm range) (pComms `S.union` qComms) range) + InternalChoice p q range -> do addDiags [mkDiag Debug "InternalChoice" proc] - pComms <- anaProcTerm p gVars lVars - qComms <- anaProcTerm q gVars lVars - return (pComms `S.union` qComms) - ExternalChoice p q _ -> + (pComms, pFQTerm) <- anaProcTerm p gVars lVars + (qComms, qFQTerm) <- anaProcTerm q gVars lVars + return (pComms `S.union` qComms, + FQProcess (InternalChoice pFQTerm qFQTerm range) (pComms `S.union` qComms) range) + ExternalChoice p q range -> do addDiags [mkDiag Debug "ExternalChoice" proc] - pComms <- anaProcTerm p gVars lVars - qComms <- anaProcTerm q gVars lVars - return (pComms `S.union` qComms) - Interleaving p q _ -> + (pComms, pFQTerm) <- anaProcTerm p gVars lVars + (qComms, qFQTerm) <- anaProcTerm q gVars lVars + return (pComms `S.union` qComms, + FQProcess (ExternalChoice pFQTerm qFQTerm range) (pComms `S.union` qComms) range) + Interleaving p q range -> do addDiags [mkDiag Debug "Interleaving" proc] - pComms <- anaProcTerm p gVars lVars - qComms <- anaProcTerm q gVars lVars - return (pComms `S.union` qComms) - SynchronousParallel p q _ -> + (pComms, pFQTerm) <- anaProcTerm p gVars lVars + (qComms, qFQTerm) <- anaProcTerm q gVars lVars + return (pComms `S.union` qComms, + FQProcess (Interleaving pFQTerm qFQTerm range) (pComms `S.union` qComms) range) + SynchronousParallel p q range -> do addDiags [mkDiag Debug "Synchronous" proc] - pComms <- anaProcTerm p gVars lVars - qComms <- anaProcTerm q gVars lVars - return (pComms `S.union` qComms) - GeneralisedParallel p es q _ -> + (pComms, pFQTerm) <- anaProcTerm p gVars lVars + (qComms, qFQTerm) <- anaProcTerm q gVars lVars + return (pComms `S.union` qComms, + FQProcess (SynchronousParallel pFQTerm qFQTerm range) (pComms `S.union` qComms) range) + GeneralisedParallel p es q range -> do addDiags [mkDiag Debug "Generalised parallel" proc] - pComms <- anaProcTerm p gVars lVars + (pComms, pFQTerm) <- anaProcTerm p gVars lVars synComms <- anaEventSet es - qComms <- anaProcTerm q gVars lVars - return (S.unions [pComms, qComms, synComms]) - AlphabetisedParallel p esp esq q _ -> + (qComms, qFQTerm) <- anaProcTerm q gVars lVars + return (S.unions [pComms, qComms, synComms], + FQProcess (GeneralisedParallel pFQTerm es qFQTerm range) (S.unions [pComms, qComms, synComms]) range) + AlphabetisedParallel p esp esq q range -> do addDiags [mkDiag Debug "Alphabetised parallel" proc] - pComms <- anaProcTerm p gVars lVars + (pComms, pFQTerm) <- anaProcTerm p gVars lVars pSynComms <- anaEventSet esp checkCommAlphaSub pSynComms pComms proc "alphabetised parallel, left" qSynComms <- anaEventSet esq - qComms <- anaProcTerm q gVars lVars + (qComms, qFQTerm) <- anaProcTerm q gVars lVars checkCommAlphaSub qSynComms qComms proc "alphabetised parallel, right" - return (pComms `S.union` qComms) - Hiding p es _ -> + return (pComms `S.union` qComms, + FQProcess (AlphabetisedParallel pFQTerm esp esq qFQTerm range) (pComms `S.union` qComms) range) + Hiding p es range -> do addDiags [mkDiag Debug "Hiding" proc] - pComms <- anaProcTerm p gVars lVars + (pComms, pFQTerm) <- anaProcTerm p gVars lVars hidComms <- anaEventSet es - return (pComms `S.union` hidComms) - RenamingProcess p r _ -> + return (pComms `S.union` hidComms, + FQProcess (Hiding pFQTerm es range) (pComms `S.union` hidComms) range) + RenamingProcess p r range -> do addDiags [mkDiag Debug "Renaming" proc] - pComms <- anaProcTerm p gVars lVars + (pComms, pFQTerm) <- anaProcTerm p gVars lVars renAlpha <- anaRenaming r - return (pComms `S.union` renAlpha) - ConditionalProcess f p q _ -> + return (pComms `S.union` renAlpha, + FQProcess (RenamingProcess pFQTerm r range) (pComms `S.union` renAlpha) range) + ConditionalProcess f p q range -> do addDiags [mkDiag Debug "Conditional" proc] - pComms <- anaProcTerm p gVars lVars - qComms <- anaProcTerm q gVars lVars + (pComms, pFQTerm) <- anaProcTerm p gVars lVars + (qComms, qFQTerm) <- anaProcTerm q gVars lVars + -- mfs is the fully qualified formula version of f mfs <- anaFormulaCspCASL (gVars `Map.union` lVars) f + addDiags [mkDiag Debug "Formula" f] + addDiags [mkDiag Debug "FQFormula" (Maybe.fromJust mfs)] let fComms = case mfs of Nothing -> S.empty Just fs -> formulaComms fs - return (S.unions [pComms, qComms, fComms]) + return (S.unions [pComms, qComms, fComms], + FQProcess (ConditionalProcess (Maybe.fromJust mfs) pFQTerm qFQTerm range) + (S.unions [pComms, qComms, fComms]) range) -- | Statically analyse a CspCASL "named process" term. @@ -582,6 +613,5 @@ ga = globAnnos sig mix = emptyMix { mixRules = makeRules ga allIds } - resF <- resolveFormula (putParen mix) (mixResolve mix) - ga (mixRules mix) frm + resF <- resolveFormula (putParen mix) (mixResolve mix) ga (mixRules mix) frm minExpFORMULA (const return) sig resF Index: /trunk/CspCASL/Print_CspCASL.hs =================================================================== --- /trunk/CspCASL/Print_CspCASL.hs (revision 10428) +++ /trunk/CspCASL/Print_CspCASL.hs (revision 11215) @@ -24,6 +24,6 @@ import CspCASL.CspCASL_Keywords -instance Pretty CspCASLSentence where - pretty _ = empty +import qualified Data.Set as S + instance Pretty CspBasicSpec where @@ -145,4 +145,13 @@ alpar_close <+> (glue pr q) ) + FQProcess p commAlpha _ -> + let commAlphaList = S.toList commAlpha + prettyComms cs = sepByCommas (map pretty cs) + in brackets(pretty p) <> text "_" <> braces (prettyComms commAlphaList) + +instance Pretty CommType where + pretty (CommTypeSort s) = pretty s + pretty (CommTypeChan (TypedChanName c s)) = parens (sepByCommas [pretty c, pretty s]) + -- glue and prec_comp decide whether the child in the parse tree needs Index: /trunk/CspCASL/Logic_CspCASL.hs =================================================================== --- /trunk/CspCASL/Logic_CspCASL.hs (revision 10910) +++ /trunk/CspCASL/Logic_CspCASL.hs (revision 11215) @@ -72,6 +72,6 @@ -- | Instance of Sentences for CspCASL (missing) instance Sentences CspCASL - AS_CspCASL.CspCASLSentence -- sentence (missing) - SignCSP.CspCASLSign -- signature + SignCSP.CspCASLSen -- sentence (missing) + SignCSP.CspCASLSign -- signature SignCSP.CspMorphism -- morphism () -- symbol (?) @@ -102,5 +102,5 @@ () -- Sublogics (missing) AS_CspCASL.CspBasicSpec -- basic_spec - AS_CspCASL.CspCASLSentence -- sentence (missing) + SignCSP.CspCASLSen -- sentence (missing) SYMB_ITEMS -- symb_items SYMB_MAP_ITEMS -- symb_map_items @@ -118,5 +118,5 @@ instance StaticAnalysis CspCASL AS_CspCASL.CspBasicSpec -- basic_spec - AS_CspCASL.CspCASLSentence -- sentence (missing) + SignCSP.CspCASLSen -- sentence (missing) SYMB_ITEMS -- symb_items SYMB_MAP_ITEMS -- symb_map_items