Changeset 11215
- Timestamp:
- 05.01.2009 15:46:06 (10 months ago)
- Location:
- trunk
- Files:
-
- 12 modified
-
Comorphisms/CASL2CspCASL.hs (modified) (3 diffs)
-
Comorphisms/CFOL2IsabelleHOL.hs (modified) (1 diff)
-
Comorphisms/CspCASL2IsabelleHOL.hs (modified) (19 diffs)
-
Comorphisms/CspCASL2Modal.hs (modified) (3 diffs)
-
CspCASL/AS_CspCASL.der.hs (modified) (3 diffs)
-
CspCASL/AS_CspCASL_Process.der.hs (modified) (4 diffs)
-
CspCASL/Logic_CspCASL.hs (modified) (3 diffs)
-
CspCASL/Print_CspCASL.hs (modified) (2 diffs)
-
CspCASL/SignCSP.hs (modified) (6 diffs)
-
CspCASL/StatAnaCSP.hs (modified) (8 diffs)
-
CspCASL/Trans_Consts.hs (modified) (2 diffs)
-
CspCASL/Trans_CspProver.hs (modified) (5 diffs)
Legend:
- Unmodified
- Added
- Removed
-
trunk/Comorphisms/CASL2CspCASL.hs
r11201 r11215 26 26 -- CspCASL 27 27 import CspCASL.Logic_CspCASL 28 import CspCASL.AS_CspCASL (CspBasicSpec (..) , CspCASLSentence, emptyCCSentence)28 import CspCASL.AS_CspCASL (CspBasicSpec (..)) 29 29 import CspCASL.SignCSP 30 30 … … 41 41 Symbol RawSymbol ProofTree 42 42 CspCASL () 43 CspBasicSpec CspCASLSen tenceSYMB_ITEMS SYMB_MAP_ITEMS43 CspBasicSpec CspCASLSen SYMB_ITEMS SYMB_MAP_ITEMS 44 44 CspCASLSign 45 45 CspMorphism … … 73 73 , pred_map = pred_map m } 74 74 75 mapSen :: CASLFORMULA -> CspCASLSen tence76 mapSen _ = emptyCCSen tence75 mapSen :: CASLFORMULA -> CspCASLSen 76 mapSen _ = emptyCCSen -
trunk/Comorphisms/CFOL2IsabelleHOL.hs
r10903 r11215 20 20 , SignTranslator 21 21 , FormulaTranslator 22 , getAssumpsToks 23 , formTrCASL 22 24 , quantifyIsa 23 25 , quantify 24 26 , transSort 27 , transRecord 25 28 , transOP_SYMB 26 29 ) where -
trunk/Comorphisms/CspCASL2IsabelleHOL.hs
r10619 r11215 27 27 import qualified Comorphisms.CFOL2IsabelleHOL as CFOL2IsabelleHOL 28 28 import Comorphisms.CFOL2IsabelleHOL(IsaTheory) 29 import CspCASL.AS_CspCASL_Process (PROCESS_NAME) 29 30 import CspCASL.Logic_CspCASL 30 31 import CspCASL.AS_CspCASL … … 49 50 instance Comorphism CspCASL2IsabelleHOL 50 51 CspCASL () 51 CspBasicSpec CspCASLSen tenceSYMB_ITEMS SYMB_MAP_ITEMS52 CspBasicSpec CspCASLSen SYMB_ITEMS SYMB_MAP_ITEMS 52 53 CspCASLSign 53 54 CspMorphism … … 71 72 72 73 -- | Translate CspCASL theories to Isabelle 73 transCCTheory :: (CspCASLSign, [Named CspCASLSen tence]) -> Result IsaTheory74 transCCTheory :: (CspCASLSign, [Named CspCASLSen]) -> Result IsaTheory 74 75 transCCTheory ccTheory = 75 76 let ccSign = fst ccTheory 76 77 ccSens = snd ccTheory 78 77 79 caslSign = ccSig2CASLSign ccSign 80 cspSign = ccSig2CspSign ccSign 81 78 82 casl2pcfol = (map_theory CASL2PCFOL.CASL2PCFOL) 79 83 pcfol2cfol = (map_theory CASL2SubCFOL.defaultCASL2SubCFOL) 80 84 cfol2isabelleHol = (map_theory CFOL2IsabelleHOL.CFOL2IsabelleHOL) 81 85 sortList = Set.toList(CASLSign.sortSet caslSign) 82 --fakeType = Type {typeId = "Fake_Type" , typeSort = [], typeArgs =[]}86 fakeType = Type {typeId = "Fake_Type" , typeSort = [], typeArgs =[]} 83 87 in do -- Remove Subsorting from the CASL part of the CspCASL specification 84 88 translation1 <- casl2pcfol (caslSign,[]) … … 87 91 -- Next Translate to IsabelleHOL code 88 92 translation3 <- cfol2isabelleHol translation2 89 -- Next add the preAlpabet construction to the IsabelleHOL code 90 return $ addCspCaslSentences ccSens 93 -- Next add the preAlphabet construction to the IsabelleHOL code 94 return $ addProcMap ccSens caslSign 95 $ addProcNameDatatype cspSign 91 96 $ addAllIntegrationTheorems sortList ccSign 92 97 $ addAllChooseFunctions sortList … … 99 104 $ addPreAlphabet sortList 100 105 $ addWarning 106 -- hack: show the casl sentences 107 -- addConst (show(ccSens)) fakeType 101 108 $ translation3 102 109 103 -- This is not implemented in a sensible way yet and is not used104 transCCSentence :: CspCASLSign -> CspCASLSen tence-> Result IsaSign.Sentence105 transCCSentence _ ( CspCASLSentence pn_ _) =110 -- BUG This is not implemented in a sensible way yet and is not used 111 transCCSentence :: CspCASLSign -> CspCASLSen -> Result IsaSign.Sentence 112 transCCSentence _ (ProcessEq pn _ _ _) = 106 113 do return (mkSen (Const (mkVName (show pn)) 107 114 (Disp (Type "byeWorld" [] []) TFun Nothing))) 108 115 109 -- | Add a list of CspCASL sentences to an Isabelle theory 110 addCspCaslSentences :: [Named CspCASLSentence] -> IsaTheory -> IsaTheory 111 addCspCaslSentences namedSens isaTh = 112 -- Create datatype for process names 113 -- crate constant 114 -- create primrec 115 -- create list of equations -- one for each sentence 116 foldl addCspCaslSentence isaTh namedSens 117 118 -- | Add a single CspCASL sentence to an Isabelle theory 119 addCspCaslSentence :: IsaTheory -> Named CspCASLSentence -> IsaTheory 120 addCspCaslSentence isaTh namedSen = 121 let sen = sentence namedSen 122 in case sen of 123 CspCASLSentence pn _ proc -> 124 let name = show pn 125 t1 = conDouble name 126 t2 = transProcess proc 127 in addDef name t1 t2 isaTh 128 129 -- Functions for adding the PreAlphabet datatype to an Isabelle theory 116 -------------------------------------------------------------------------- 117 -- Functions for adding the process name datatype to an Isabelle theory -- 118 -------------------------------------------------------------------------- 119 120 -- | Add process name datatype which has a constructor for each 121 -- process name (along with the arguments for the process) in the 122 -- CspCASL Signature to an Isabelle theory 123 addProcNameDatatype :: CspSign -> IsaTheory -> IsaTheory 124 addProcNameDatatype cspSign isaTh = 125 let -- Create a list of pairs of process names and thier profiles 126 procSetList = Map.toList (procSet cspSign) 127 procNameDomainEntry = mkProcNameDE procSetList 128 in updateDomainTab procNameDomainEntry isaTh 129 130 131 -- | Make a proccess name Domain Entry from ... 132 mkProcNameDE :: [(PROCESS_NAME, ProcProfile)] -> DomainEntry 133 mkProcNameDE processes = 134 let -- The a list of pairs of constructors and their arguments 135 constructors = map mk_cons processes 136 -- Take a proccess name and its argument sorts (also its 137 -- commAlpha - thrown away) and make a pair representing the 138 -- constructor and the argument types 139 mk_cons (procName, (ProcProfile sorts _)) = 140 (mkVName (mkProcNameConstructor procName), map sortToTyp sorts) 141 -- Turn a sort in to a Typ suitable for the domain entry The 142 -- processes need to have arguments of the bar variants of 143 -- the sorts not the original sorts 144 sortToTyp sort = Type {typeId = mkSortBarString sort, 145 typeSort = [isaTerm], 146 typeArgs = []} 147 in 148 (procNameType, constructors) 149 150 ------------------------------------------------------------------------- 151 -- Functions adding the process map fucntion to an Isabelle theory -- 152 ------------------------------------------------------------------------- 153 154 -- | Add the fucction procMap to an Isabelle theory. This function 155 -- maps process names to real processes build using the same names 156 -- and the alphabet i.e., ProcName => (ProcName, Alphabet) proc. We 157 -- need to know the CspCASL sentences and the casl signature (data 158 -- part) 159 addProcMap :: [Named CspCASLSen] -> CASLSign.Sign () () -> IsaTheory -> 160 IsaTheory 161 addProcMap namedSens caslSign isaTh = 162 let 163 -- Build new Isabelle theory with additional constant 164 isaThWithConst = addConst procMapS procMapType isaTh 165 -- Get the plain sentences from the named senetences 166 sens = map (\namedsen -> sentence namedsen) namedSens 167 -- Filter so we only have proccess equations and no CASL senetences 168 processEqs = filter isProcessEq sens 169 -- the term representing the procMap that tajes a term as a 170 -- parameter 171 procMapTerm = termAppl (conDouble procMapS) 172 -- Make a single equation for the primrec from a process equation 173 -- BUG HERE - this next part is not right - underscore is bad 174 mkEq (ProcessEq procName vars _ proc) = 175 let -- Make the name (string) for this process 176 procNameString = convertProcessName2String procName 177 -- Change the name to a term 178 procNameTerm = conDouble procNameString 179 -- Turn the list of variables into a list of Isabelle 180 -- free variables 181 varTerms = [] -- BUG - should be somehting like map (\x -> mkFree (show x)) vars 182 -- Make a lhs term built of termAppl applied to the 183 -- proccess name and the variables 184 lhs = procMapTerm (foldl termAppl (procNameTerm) varTerms) 185 rhs = transProcess caslSign proc 186 in binEq lhs rhs 187 -- Build equations for primrec using process equations 188 eqs = map mkEq processEqs 189 in addPrimRec eqs isaThWithConst 190 191 ------------------------------------------------------------------------- 192 -- Functions for adding the PreAlphabet datatype to an Isabelle theory -- 193 ------------------------------------------------------------------------- 130 194 131 195 -- | Add the PreAlphabet (built from a list of sorts) to an Isabelle theory … … 142 206 (mkVName (mkPreAlphabetConstructor sort), 143 207 [Type {typeId = convertSort2String sort, 144 145 208 typeSort = [isaTerm], 209 typeArgs = []}]) 146 210 ) sorts 147 211 ) 148 212 149 -- Functions for adding the eq functions and the compare_with 150 -- functions to an Isabelle theory 213 ---------------------------------------------------------------- 214 -- Functions for adding the eq functions and the compare_with -- 215 -- functions to an Isabelle theory -- 216 ---------------------------------------------------------------- 151 217 152 218 -- | Add the eq function to an Isabelle theory using a list of sorts 153 219 addEqFun :: [SORT] -> IsaTheory -> IsaTheory 154 220 addEqFun sortList isaTh = 155 let preAlphabetType = Type {typeId = preAlphabetS, 156 typeSort = [], 157 typeArgs =[]} 158 eqtype = mkFunType preAlphabetType $ mkFunType preAlphabetType boolType 221 let eqtype = mkFunType preAlphabetType $ mkFunType preAlphabetType boolType 159 222 isaThWithConst = addConst eq_PreAlphabetS eqtype isaTh 160 223 mkEq sort = … … 183 246 addCompareWithFun ccSign isaTh sort = 184 247 let sortList = Set.toList(CASLSign.sortSet ccSign) 185 preAlphabetType = Type {typeId = preAlphabetS,186 typeSort = [],187 typeArgs =[]}188 248 sortType = Type {typeId = convertSort2String sort, typeSort = [], 189 249 typeArgs =[]} … … 232 292 in addPrimRec eqs isaThWithConst 233 293 234 -- Functions for producing the Justification theorems 294 -------------------------------------------------------- 295 -- Functions for producing the Justification theorems -- 296 -------------------------------------------------------- 235 297 236 298 -- | Add all justification theorems to an Isabelle Theory. We need to … … 409 471 in addThreomWithProof name thmConds thmConcl proof' isaTh 410 472 473 -------------------------------------------------------------- 474 -- Functions for producing instances of equivalence classes -- 475 -------------------------------------------------------------- 476 411 477 -- | Function to add preAlphabet as an equivalence relation to an 412 478 -- Isabelle theory … … 434 500 $ isaTh 435 501 502 ------------------------------------------------------------- 503 -- Functions for producing the alphabet type and bar types -- 504 ------------------------------------------------------------- 505 436 506 -- | Function to add the Alphabet type (type synonym) to an Isabelle theory 437 507 addAlphabetType :: IsaTheory -> IsaTheory 438 508 addAlphabetType isaTh = 439 let preAlphabetType = Type {typeId = preAlphabetS, 440 typeSort = [], 441 typeArgs =[]} 442 preAlphabetQuotType = Type {typeId = quotS, 443 typeSort = [], 444 typeArgs =[preAlphabetType]} 445 isaTh_sign = fst isaTh 509 let isaTh_sign = fst isaTh 446 510 isaTh_sign_tsig = tsig isaTh_sign 447 511 myabbrs = abbrs isaTh_sign_tsig … … 460 524 addBarType :: IsaTheory -> SORT -> IsaTheory 461 525 addBarType isaTh sort = 462 let sortBarString = convertSort2String sort ++ barExtS526 let sortBarString = mkSortBarString sort 463 527 barType = Type {typeId = sortBarString, typeSort = [], typeArgs =[]} 464 alphabetType = Type {typeId = alphabetS,465 typeSort = [],466 typeArgs =[]}467 528 isaTh_sign = fst isaTh 468 529 isaTh_sen = snd isaTh … … 538 599 Apply (SubgoalTac subgoalTacTerm), 539 600 Apply(Simp), 540 Apply( Other ("unfold " ++ quotEqualityS)),601 Apply(SimpAdd Nothing [quotEqualityS]), 541 602 Apply(Other ("unfold "++ preAlphabetSimS 542 603 ++ "_def")), … … 544 605 Done 545 606 in addThreomWithProof chooseFunName thmConds thmConcl proof' isaTh 607 608 ------------------------------------------------------ 609 -- Functions for producing the integration theorems -- 610 ------------------------------------------------------ 546 611 547 612 -- | Add all the integration theorems. We need to know all the sorts … … 573 638 then false 574 639 else 575 -- pick any common sort - we should pick the top most one. 640 -- BUG pick any common sort for now (this does hold 641 -- and is valid) we should pick the top most one. 576 642 let s' = head commonSuperList 577 643 in binEq (mkInjection s1 s' x) (mkInjection s2 s' y) … … 589 655 in addThreomWithProof "IntegrationTheorem_A" thmConds thmConcl proof' isaTh 590 656 591 -- Function to help keep strings consistent 592 657 ---------------------------------------------- 658 -- Function to help keep strings consistent -- 659 ---------------------------------------------- 660 661 -- | String of the name of the function to compare eqaulity of two 662 -- elements of the PreAlphabet 593 663 eq_PreAlphabetS :: String 594 664 eq_PreAlphabetS = "eq_PreAlphabet" … … 603 673 quotEqualityS :: String 604 674 quotEqualityS = "quot_equality" 605 606 preAlphabetS :: String607 preAlphabetS = "PreAlphabet"608 609 quotS :: String610 quotS = "quot"611 675 612 676 reflexivityTheoremS :: String … … 769 833 -- Function that returns the constructor of PreAlphabet for a given sort 770 834 mkPreAlphabetConstructor :: SORT -> String 771 mkPreAlphabetConstructor sort = "C_" ++ (show sort) 835 mkPreAlphabetConstructor sort = "C_" ++ (convertSort2String sort) 836 837 mkProcNameConstructor :: PROCESS_NAME -> String 838 mkProcNameConstructor pn = show pn 772 839 773 840 -- Function that takes a sort and outputs a the function name for the … … 781 848 mkChooseFunName sort = ("choose_" ++ (mkPreAlphabetConstructor sort)) 782 849 783 -- Functions for manipulating an Isabelle theory 850 851 852 -- Converts a SORT in to the corresponding bar sort represented as a 853 -- string 854 mkSortBarString :: SORT -> String 855 mkSortBarString s = convertSort2String s ++ barExtS 856 --------------------------------------------------- 857 -- Functions for manipulating an Isabelle theory -- 858 --------------------------------------------------- 784 859 785 860 -- Add a single constant to the signature of an Isabelle theory … … 845 920 in (isaTh_sign, isaTh_sen ++ [namedSen]) 846 921 847 -- Code below this line is junk 922 ---------------------------------- 923 -- Code below this line is junk -- 924 ---------------------------------- 848 925 849 926 -- Add a warning to an Isabelle theory -
trunk/Comorphisms/CspCASL2Modal.hs
r11201 r11215 28 28 import CspCASL.Logic_CspCASL 29 29 import CspCASL.SignCSP 30 import CspCASL.AS_CspCASL (CspBasicSpec (..) , CspCASLSentence)30 import CspCASL.AS_CspCASL (CspBasicSpec (..)) 31 31 32 32 -- ModalCASL … … 42 42 instance Comorphism CspCASL2Modal 43 43 CspCASL () 44 CspBasicSpec CspCASLSen tenceSYMB_ITEMS SYMB_MAP_ITEMS44 CspBasicSpec CspCASLSen SYMB_ITEMS SYMB_MAP_ITEMS 45 45 CspCASLSign 46 46 CspMorphism … … 82 82 83 83 84 mapSen :: CspCASLSen tence-> ModalFORMULA84 mapSen :: CspCASLSen -> ModalFORMULA 85 85 mapSen _f = True_atom nullRange 86 86 -
trunk/CspCASL/AS_CspCASL.der.hs
r10471 r11215 14 14 module CspCASL.AS_CspCASL where 15 15 16 import Common.Doc 17 import Common.DocUtils 16 18 import Common.Id 17 19 18 import CASL.AS_Basic_CASL (SORT, VAR )20 import CASL.AS_Basic_CASL (SORT, VAR, FORMULA) 19 21 20 22 import CspCASL.AS_CspCASL_Process (CHANNEL_NAME, COMM_TYPE, PROCESS(..), 21 23 PROCESS_NAME) 22 23 import Common.Id24 24 25 25 -- DrIFT command … … 34 34 deriving Show 35 35 36 data PROC_ALPHABET = ProcAlphabet [COMM_TYPE] Range 37 deriving (Show,Ord, Eq) 38 36 39 data PROC_ITEM = Proc_Decl PROCESS_NAME PROC_ARGS PROC_ALPHABET 37 40 | Proc_Eq PARM_PROCNAME PROCESS … … 42 45 data PARM_PROCNAME = ParmProcname PROCESS_NAME [VAR] 43 46 deriving Show 44 45 data PROC_ALPHABET = ProcAlphabet [COMM_TYPE] Range46 deriving Show47 48 -- Sentences49 50 data CspCASLSentence = CspCASLSentence PROCESS_NAME [VAR] PROCESS51 deriving (Show, Eq, Ord)52 53 emptyProcName :: PROCESS_NAME54 emptyProcName = mkSimpleId "empty"55 56 emptyCCSentence :: CspCASLSentence57 emptyCCSentence = CspCASLSentence emptyProcName []58 (NamedProcess emptyProcName [] nullRange) -
trunk/CspCASL/AS_CspCASL_Process.der.hs
r10428 r11215 21 21 PROCESS_NAME, 22 22 RENAMING, 23 CommAlpha(..), 24 CommType(..), 25 TypedChanName(..) 23 26 ) where 24 27 25 28 import CASL.AS_Basic_CASL (FORMULA, SORT, TERM, VAR) 26 29 import Common.Id 30 import qualified Data.Set as Set 27 31 28 32 -- DrIFT command … … 47 51 type RENAMING = [Id] 48 52 49 50 53 type CHANNEL_NAME = SIMPLE_ID 51 54 … … 54 57 type COMM_TYPE = SIMPLE_ID 55 58 59 -- | A process communication alphabet consists of a set of sort names 60 -- and typed channel names. 61 data TypedChanName = TypedChanName CHANNEL_NAME SORT 62 deriving (Eq, Ord, Show) 63 64 data CommType = CommTypeSort SORT 65 | CommTypeChan TypedChanName 66 deriving (Eq, Ord) 67 68 instance Show CommType where 69 show (CommTypeSort s) = show s 70 show (CommTypeChan (TypedChanName c s)) = show (c, s) 71 72 type CommAlpha = Set.Set CommType 56 73 57 74 -- |CSP-CASL process expressions. … … 96 113 -- | Named process 97 114 | NamedProcess PROCESS_NAME [TERM ()] Range 115 -- | Fully qualified process. The range here shall be the same as 116 -- | in the process. 117 | FQProcess PROCESS CommAlpha Range 98 118 deriving (Eq, Ord, Show) -
trunk/CspCASL/Logic_CspCASL.hs
r10910 r11215 72 72 -- | Instance of Sentences for CspCASL (missing) 73 73 instance Sentences CspCASL 74 AS_CspCASL.CspCASLSentence-- sentence (missing)75 SignCSP.CspCASLSign 74 SignCSP.CspCASLSen -- sentence (missing) 75 SignCSP.CspCASLSign -- signature 76 76 SignCSP.CspMorphism -- morphism 77 77 () -- symbol (?) … … 102 102 () -- Sublogics (missing) 103 103 AS_CspCASL.CspBasicSpec -- basic_spec 104 AS_CspCASL.CspCASLSentence-- sentence (missing)104 SignCSP.CspCASLSen -- sentence (missing) 105 105 SYMB_ITEMS -- symb_items 106 106 SYMB_MAP_ITEMS -- symb_map_items … … 118 118 instance StaticAnalysis CspCASL 119 119 AS_CspCASL.CspBasicSpec -- basic_spec 120 AS_CspCASL.CspCASLSentence-- sentence (missing)120 SignCSP.CspCASLSen -- sentence (missing) 121 121 SYMB_ITEMS -- symb_items 122 122 SYMB_MAP_ITEMS -- symb_map_items -
trunk/CspCASL/Print_CspCASL.hs
r10428 r11215 24 24 import CspCASL.CspCASL_Keywords 25 25 26 i nstance Pretty CspCASLSentence where27 pretty _ = empty 26 import qualified Data.Set as S 27 28 28 29 29 instance Pretty CspBasicSpec where … … 145 145 alpar_close <+> (glue pr q) 146 146 ) 147 FQProcess p commAlpha _ -> 148 let commAlphaList = S.toList commAlpha 149 prettyComms cs = sepByCommas (map pretty cs) 150 in brackets(pretty p) <> text "_" <> braces (prettyComms commAlphaList) 151 152 instance Pretty CommType where 153 pretty (CommTypeSort s) = pretty s 154 pretty (CommTypeChan (TypedChanName c s)) = parens (sepByCommas [pretty c, pretty s]) 155 147 156 148 157 -- glue and prec_comp decide whether the child in the parse tree needs -
trunk/CspCASL/SignCSP.hs
r10827 r11215 17 17 module CspCASL.SignCSP where 18 18 19 import CspCASL.AS_CspCASL_Process (CHANNEL_NAME, PROCESS_NAME) 20 21 import CASL.AS_Basic_CASL (SORT) 19 import CspCASL.AS_CspCASL_Process (CHANNEL_NAME, PROCESS_NAME, 20 PROCESS(..), CommAlpha(..), CommType(..), TypedChanName(..)) 21 22 import CspCASL.AS_CspCASL () 23 import CspCASL.Print_CspCASL 24 25 import CASL.AS_Basic_CASL (FORMULA, SORT) 22 26 import CASL.Sign (emptySign, Sign, extendedInfo, sortRel) 23 27 import CASL.Morphism (Morphism) 24 28 25 import qualified Common.Doc as Doc 26 import qualified Common.DocUtils as DocUtils 27 import Common.Id (Id, SIMPLE_ID) 29 import Common.AS_Annotation (Named) 30 31 import Common.Doc 32 import Common.DocUtils 33 34 import Common.Id (Id, SIMPLE_ID, mkSimpleId, nullRange) 28 35 import Common.Lib.Rel (predecessors) 29 36 import Common.Result … … 38 45 deriving (Eq, Show) 39 46 40 -- | A process communication alphabet consists of a set of sort names41 -- and typed channel names.42 data TypedChanName = TypedChanName CHANNEL_NAME SORT43 deriving (Eq, Ord, Show)44 data CommType = CommTypeSort SORT45 | CommTypeChan TypedChanName46 deriving (Eq, Ord)47 instance Show CommType where48 show (CommTypeSort s) = show s49 show (CommTypeChan (TypedChanName c s)) = show (c, s)50 51 type CommAlpha = Set.Set CommType52 53 47 type ChanNameMap = Map.Map CHANNEL_NAME SORT 54 48 type ProcNameMap = Map.Map PROCESS_NAME ProcProfile 55 49 type ProcVarMap = Map.Map SIMPLE_ID SORT 50 type ProcVarList = [(SIMPLE_ID, SORT)] 56 51 57 52 -- Close a communication alphabet under CASL subsort … … 99 94 { chans :: ChanNameMap 100 95 , procSet :: ProcNameMap 96 -- | Added for uniformity to the CASL static analysis. After 97 -- static analysis this is the empty list. 98 , ccSentences :: [Named CspCASLSen] 101 99 } deriving (Eq, Show) 102 100 … … 107 105 ccSig2CASLSign :: CspCASLSign -> Sign () () 108 106 ccSig2CASLSign sigma = sigma { extendedInfo = () } 107 108 ccSig2CspSign :: CspCASLSign -> CspSign 109 ccSig2CspSign sigma = extendedInfo sigma 109 110 110 111 -- | Empty CspCASL signature. … … 117 118 { chans = Map.empty 118 119 , procSet = Map.empty 120 , ccSentences =[] 119 121 } 120 122 … … 170 172 171 173 -- dummy instances, need to be elaborated! 172 instance DocUtils.Pretty CspSign where 173 pretty = Doc.text . show 174 instance DocUtils.Pretty CspAddMorphism where 175 pretty = Doc.text . show 174 instance Pretty CspSign where 175 pretty = text . show 176 instance Pretty CspAddMorphism where 177 pretty = text . show 178 179 -- Sentences 180 181 -- A CspCASl senetence is either a CASL formula or a Procsses 182 -- equation. A process equation has on the LHS a process name, a list 183 -- of parameters which are qualified variables (which are terms), a 184 -- constituent communication alphabet and finally on the RHS a fully 185 -- qualified process. 186 data CspCASLSen = CASLSen (FORMULA ()) 187 | ProcessEq PROCESS_NAME ProcVarList CommAlpha PROCESS 188 deriving (Show, Eq, Ord) 189 190 instance Pretty CspCASLSen where 191 -- Not implemented yet - the pretty printing of the casl sentences 192 pretty(CASLSen _) = text "Pretty printing for CASLSen not implemented yet" 193 pretty(ProcessEq pn varList alpha proc) = 194 let varDoc = if (null varList) 195 then empty 196 else parens $ sepByCommas $ map pretty (map fst varList) 197 in pretty pn <+> varDoc <+> equals <+> pretty proc 198 199 emptyCCSen :: CspCASLSen 200 emptyCCSen = 201 let emptyProcName = mkSimpleId "empty" 202 emptyVarList = [] 203 emptyAlphabet = Set.empty 204 emptyProc = Skip nullRange 205 in ProcessEq emptyProcName emptyVarList emptyAlphabet emptyProc 206 207 isCASLSen :: CspCASLSen -> Bool 208 isCASLSen (CASLSen _) = True 209 isCASLSen _ = False 210 211 isProcessEq :: CspCASLSen -> Bool 212 isProcessEq (ProcessEq _ _ _ _) = True 213 isProcessEq _ = False 214 -
trunk/CspCASL/StatAnaCSP.hs
r11201 r11215 21 21 import qualified Data.Maybe as Maybe 22 22 import qualified Data.Set as S 23 23 -- liam added the following, they should be deleted from imports when 24 -- liams temp code is removed: Op_name mkSimpleId mkInfix OP_SYMB(..), 25 -- OP_TYPE(..) 24 26 import CASL.AS_Basic_CASL (FORMULA(..), OpKind(..), SORT, TERM(..), VAR, 25 27 VAR_DECL(..)) … … 34 36 import Common.ConvertGlobalAnnos 35 37 import qualified Common.Lib.Rel as Rel 36 import Common.Id (getRange, Id, simpleIdToId, nullRange , mkSimpleId)38 import Common.Id (getRange, Id, simpleIdToId, nullRange) 37 39 import Common.Lib.State 38 40 import Common.ExtSign … … 44 46 import CspCASL.SignCSP 45 47 48 import qualified Data.Set as Set 49 46 50 basicAnalysisCspCASL :: (CspBasicSpec, CspCASLSign, GlobalAnnos) 47 51 -> Result (CspBasicSpec, ExtSign CspCASLSign (), 48 [Named CspCASLSen tence])49 basicAnalysisCspCASL (cc, sigma, ga) = do52 [Named CspCASLSen]) 53 basicAnalysisCspCASL (cc, sigma, ga) = 50 54 let Result es mga = mergeGlobalAnnos ga $ globAnnos sigma 51 55 (_, accSig) = runState (ana_BASIC_CSP cc) $ case mga of … … 53 57 Just nga -> sigma { globAnnos = nga } 54 58 ds = reverse $ envDiags accSig 55 Result (es ++ ds) (Just ()) -- insert diagnostics 56 return (cc, mkExtSign accSig, [makeNamed "empty_sentence" emptyCCSentence, 57 makeNamed "StopProcSen" stopProc, 58 makeNamed "GParProcSen" gParProc, 59 makeNamed "AParProcSen" aParProc, 60 makeNamed "StopProcSen" seqProc]) 61 where 62 stopProc = CspCASLSentence (mkSimpleId "stopProc") [] (Stop nullRange) 63 seqProc = CspCASLSentence (mkSimpleId "seqProc") [] 64 (Sequential (Stop nullRange) 65 (Stop nullRange) nullRange) 66 gParProc = CspCASLSentence (mkSimpleId "gParProc") [] 67 (GeneralisedParallel (Stop nullRange) 68 (EventSet [mkSimpleId "S"] nullRange) 69 (Skip nullRange) nullRange) 70 aParProc = CspCASLSentence (mkSimpleId "gParProc") [] 71 (AlphabetisedParallel (Stop nullRange) 72 (EventSet [mkSimpleId "T"] nullRange) 73 (EventSet [mkSimpleId "U"] nullRange) 74 (Skip nullRange) nullRange) 59 -- Extract process equations only. 60 ext = extendedInfo accSig 61 ccsents = reverse $ ccSentences ext 62 -- Clean signature here 63 cleanSig = accSig 64 { extendedInfo = ext { ccSentences = []}} 65 in Result (es ++ ds) $ 66 Just (cc, mkExtSign cleanSig, ccsents) 75 67 76 68 ana_BASIC_CSP :: CspBasicSpec -> State CspCASLSign () … … 102 94 103 95 -- | Statically analyse a CspCASL channel declaration. 104 anaChanDecl :: CHANNEL_DECL -> State CspCASLSign CHANNEL_DECL96 anaChanDecl :: CHANNEL_DECL -> State CspCASLSign () 105 97 anaChanDecl (ChannelDecl chanNames chanSort) = do 106 98 checkSorts [chanSort] -- check channel sort is known … … 113 105 , envDiags = vds 114 106 } 115 return ( ChannelDecl chanNames chanSort)107 return () 116 108 117 109 -- | Statically analyse a CspCASL channel name. … … 178 170 sig <- get 179 171 let ext = extendedInfo sig 172 ccsens = ccSentences ext 180 173 procDecls = procSet ext 181 174 prof = pn `Map.lookup` procDecls 182 175 case prof of 183 -- Only analyse a process if its name (and thus profile) is known 184 Just (ProcProfile procArgs procAlpha) -> 185 do gVars <- anaProcVars pn procArgs vs -- compute global vars 186 termAlpha <- anaProcTerm proc gVars Map.empty 187 checkCommAlphaSub termAlpha procAlpha proc "process equation" 188 return () 189 Nothing -> 190 do addDiags [mkDiag Error "process equation for unknown process" pn] 191 return () 192 vds <- gets envDiags 193 put sig { envDiags = vds } 176 -- Only analyse a process if its name (and thus profile) is known 177 Just (ProcProfile procArgs procAlpha) -> 178 do gVars <- anaProcVars pn procArgs vs -- compute global vars 179 (termAlpha, fqProc) <- anaProcTerm proc (Map.fromList gVars) Map.empty 180 checkCommAlphaSub termAlpha procAlpha proc "process equation" 181 -- Save the diags from the checkCommAlphaSub 182 vds <- gets envDiags 183 -- put CspCASL Sentences back in to the state with new sentence 184 put sig {envDiags = vds, extendedInfo = 185 ext { ccSentences = 186 -- BUG - What should the constituent 187 -- alphabet be for this process? 188 -- probably the same as the inner one! 189 (makeNamed ("ProcHugo") 190 (ProcessEq pn gVars 191 Set.empty 192 fqProc)):ccsens 193 } 194 } 195 return () 196 Nothing -> 197 do addDiags [mkDiag Error "process equation for unknown process" pn] 198 return () 194 199 return () 195 200 196 201 -- | Statically analyse a CspCASL process equation's global variable 197 202 -- names. 198 anaProcVars :: PROCESS_NAME -> [SORT] -> [VAR] -> State CspCASLSign ProcVar Map203 anaProcVars :: PROCESS_NAME -> [SORT] -> [VAR] -> State CspCASLSign ProcVarList 199 204 anaProcVars pn ss vs = do 200 205 case (compare (length ss) (length vs)) of 201 206 LT -> do addDiags [mkDiag Error "too many process arguments" pn] 202 return Map.empty207 return [] 203 208 GT -> do addDiags [mkDiag Error "not enough process arguments" pn] 204 return Map.empty205 EQ -> Monad.foldM anaProcVar Map.empty(zip vs ss)209 return [] 210 EQ -> Monad.foldM anaProcVar [] (zip vs ss) 206 211 207 212 -- | Statically analyse a CspCASL process-global variable name. 208 anaProcVar :: ProcVar Map -> (VAR, SORT) -> State CspCASLSign ProcVarMap213 anaProcVar :: ProcVarList -> (VAR, SORT) -> State CspCASLSign ProcVarList 209 214 anaProcVar old (v, s) = do 210 if v ` Map.member` old211 then do addDiags [mkDiag Error "process arg declared more than once" v]215 if v `elem` (map fst old) 216 then do addDiags [mkDiag Error "process argument declared more than once" v] 212 217 return old 213 else return ( Map.insert v s old)218 else return (old ++ [(v, s)]) 214 219 215 220 -- Static analysis of process terms 216 221 222 -- BUG in fucntion below 223 -- not returing FQProcesses 217 224 -- | Statically analyse a CspCASL process term. 225 -- The process that is returned is a fully qualified process. 218 226 anaProcTerm :: PROCESS -> ProcVarMap -> ProcVarMap -> 219 State CspCASLSign CommAlpha227 State CspCASLSign (CommAlpha, PROCESS) 220 228 anaProcTerm proc gVars lVars = case proc of 221 NamedProcess name args _->229 NamedProcess name args range -> 222 230 do addDiags [mkDiag Debug "Named process" proc] 223 231 al <- anaNamedProc proc name args (lVars `Map.union` gVars) 224 return al 225 Skip _ -> 232 return (al, 233 FQProcess (NamedProcess name args range) al range) 234 Skip range -> 226 235 do addDiags [mkDiag Debug "Skip" proc] 227 return S.empty 228 Stop _ -> 236 return (S.empty, 237 FQProcess (Skip range) S.empty range) 238 Stop range -> 229 239 do addDiags [mkDiag Debug "Stop" proc] 230 return S.empty 231 Div _ -> 240 return (S.empty, 241 FQProcess (Stop range) S.empty range) 242 Div range -> 232 243 do addDiags [mkDiag Debug "Div" proc] 233 return S.empty 234 Run es _ -> 244 return (S.empty, 245 FQProcess (Div range) S.empty range) 246 Run es range -> 235 247 do addDiags [mkDiag Debug "Run" proc] 236 248 comms <- anaEventSet es 237 return comms 238 Chaos es _ -> 249 return (comms, 250 FQProcess (Run es range) comms range) 251 Chaos es range -> 239 252 do addDiags [mkDiag Debug "Chaos" proc] 240 253 comms <- anaEventSet es 241 return comms 242 PrefixProcess e p _ -> 254 return (comms, 255 FQProcess (Chaos es range) comms range) 256 PrefixProcess e p range -> 243 257 do addDiags [mkDiag Debug "Prefix" proc] 244 258 (evComms, rcvMap) <- anaEvent e (lVars `Map.union` gVars) 245 comms <- anaProcTerm p gVars (rcvMap `Map.union` lVars) 246 return (comms `S.union` evComms) 247 InternalPrefixProcess v s p _ -> 259 (comms, pFQTerm) <- anaProcTerm p gVars (rcvMap `Map.union` lVars) 260 return (comms `S.union` evComms, 261 FQProcess (PrefixProcess e pFQTerm range) (comms `S.union` evComms) range) 262 InternalPrefixProcess v s p range -> 248 263 do addDiags [mkDiag Debug "Internal prefix" proc] 249 264 checkSorts [s] -- check sort is known 250 comms <- anaProcTerm p gVars (Map.insert v s lVars) 251 return (S.insert (CommTypeSort s) comms) 252 ExternalPrefixProcess v s p _ -> 265 (comms, pFQTerm) <- anaProcTerm p gVars (Map.insert v s lVars) 266 return (S.insert (CommTypeSort s) comms, 267 FQProcess (InternalPrefixProcess v s pFQTerm range) (S.insert (CommTypeSort s) comms) range) 268 ExternalPrefixProcess v s p range -> 253 269 do addDiags [mkDiag Debug "External prefix" proc] 254 270 checkSorts [s] -- check sort is known 255 comms <- anaProcTerm p gVars (Map.insert v s lVars) 256 return (S.insert (CommTypeSort s) comms) 257 Sequential p q _ -> 271 (comms, pFQTerm) <- anaProcTerm p gVars (Map.insert v s lVars) 272 return (S.insert (CommTypeSort s) comms, 273 FQProcess (ExternalPrefixProcess v s pFQTerm range) (S.insert (CommTypeSort s) comms) range) 274 Sequential p q range -> 258 275 do addDiags [mkDiag Debug "Sequential" proc] 259 pComms <- anaProcTerm p gVars lVars 260 qComms <- anaProcTerm q gVars Map.empty 261 return (pComms `S.union` qComms) 262 InternalChoice p q _ -> 276 (pComms, pFQTerm) <- anaProcTerm p gVars lVars 277 (qComms, qFQTerm) <- anaProcTerm q gVars Map.empty 278 return (pComms `S.union` qComms, 279 FQProcess (Sequential pFQTerm qFQTerm range) (pComms `S.union` qComms) range) 280 InternalChoice p q range -> 263 281 do addDiags [mkDiag Debug "InternalChoice" proc] 264 pComms <- anaProcTerm p gVars lVars 265 qComms <- anaProcTerm q gVars lVars 266 return (pComms `S.union` qComms) 267 ExternalChoice p q _ -> 282 (pComms, pFQTerm) <- anaProcTerm p gVars lVars 283 (qComms, qFQTerm) <- anaProcTerm q gVars lVars 284 return (pComms `S.union` qComms, 285 FQProcess (InternalChoice pFQTerm qFQTerm range) (pComms `S.union` qComms) range) 286 ExternalChoice p q range -> 268 287 do addDiags [mkDiag Debug "ExternalChoice" proc] 269 pComms <- anaProcTerm p gVars lVars 270 qComms <- anaProcTerm q gVars lVars 271 return (pComms `S.union` qComms) 272 Interleaving p q _ -> 288 (pComms, pFQTerm) <- anaProcTerm p gVars lVars 289 (qComms, qFQTerm) <- anaProcTerm q gVars lVars 290 return (pComms `S.union` qComms, 291 FQProcess (ExternalChoice pFQTerm qFQTerm range) (pComms `S.union` qComms) range) 292 Interleaving p q range -> 273 293 do addDiags [mkDiag Debug "Interleaving" proc] 274 pComms <- anaProcTerm p gVars lVars 275 qComms <- anaProcTerm q gVars lVars 276 return (pComms `S.union` qComms) 277 SynchronousParallel p q _ -> 294 (pComms, pFQTerm) <- anaProcTerm p gVars lVars 295 (qComms, qFQTerm) <- anaProcTerm q gVars lVars 296 return (pComms `S.union` qComms, 297 FQProcess (Interleaving pFQTerm qFQTerm range) (pComms `S.union` qComms) range) 298 SynchronousParallel p q range -> 278 299 do addDiags [mkDiag Debug "Synchronous" proc] 279 pComms <- anaProcTerm p gVars lVars 280 qComms <- anaProcTerm q gVars lVars 281 return (pComms `S.union` qComms) 282 GeneralisedParallel p es q _ -> 300 (pComms, pFQTerm) <- anaProcTerm p gVars lVars 301 (qComms, qFQTerm) <- anaProcTerm q gVars lVars 302 return (pComms `S.union` qComms, 303 FQProcess (SynchronousParallel pFQTerm qFQTerm range) (pComms `S.union` qComms) range) 304 GeneralisedParallel p es q range -> 283 305 do addDiags [mkDiag Debug "Generalised parallel" proc] 284 pComms<- anaProcTerm p gVars lVars306 (pComms, pFQTerm) <- anaProcTerm p gVars lVars 285 307 synComms <- anaEventSet es 286 qComms <- anaProcTerm q gVars lVars 287 return (S.unions [pComms, qComms, synComms]) 288 AlphabetisedParallel p esp esq q _ -> 308 (qComms, qFQTerm) <- anaProcTerm q gVars lVars 309 return (S.unions [pComms, qComms, synComms], 310 FQProcess (GeneralisedParallel pFQTerm es qFQTerm range) (S.unions [pComms, qComms, synComms]) range) 311 AlphabetisedParallel p esp esq q range -> 289 312 do addDiags [mkDiag Debug "Alphabetised parallel" proc] 290 pComms<- anaProcTerm p gVars lVars313 (pComms, pFQTerm) <- anaProcTerm p gVars lVars 291 314 pSynComms <- anaEventSet esp 292 315 checkCommAlphaSub pSynComms pComms proc 293 316 "alphabetised parallel, left" 294 317 qSynComms <- anaEventSet esq 295 qComms<- anaProcTerm q gVars lVars318 (qComms, qFQTerm) <- anaProcTerm q gVars lVars 296 319 checkCommAlphaSub qSynComms qComms proc 297 320 "alphabetised parallel, right" 298 return (pComms `S.union` qComms) 299 Hiding p es _ -> 321 return (pComms `S.union` qComms, 322 FQProcess (AlphabetisedParallel pFQTerm esp esq qFQTerm range) (pComms `S.union` qComms) range) 323 Hiding p es range -> 300 324 do addDiags [mkDiag Debug "Hiding" proc] 301 pComms<- anaProcTerm p gVars lVars325 (pComms, pFQTerm) <- anaProcTerm p gVars lVars 302 326 hidComms <- anaEventSet es 303 return (pComms `S.union` hidComms) 304 RenamingProcess p r _ -> 327 return (pComms `S.union` hidComms, 328 FQProcess (Hiding pFQTerm es range) (pComms `S.union` hidComms) range) 329 RenamingProcess p r range -> 305 330 do addDiags [mkDiag Debug "Renaming" proc] 306 pComms<- anaProcTerm p gVars lVars331 (pComms, pFQTerm) <- anaProcTerm p gVars lVars 307 332 renAlpha <- anaRenaming r 308 return (pComms `S.union` renAlpha) 309 ConditionalProcess f p q _ -> 333 return (pComms `S.union` renAlpha, 334 FQProcess (RenamingProcess pFQTerm r range) (pComms `S.union` renAlpha) range) 335 ConditionalProcess f p q range -> 310 336 do addDiags [mkDiag Debug "Conditional" proc] 311 pComms <- anaProcTerm p gVars lVars 312 qComms <- anaProcTerm q gVars lVars 337 (pComms, pFQTerm) <- anaProcTerm p gVars lVars 338 (qComms, qFQTerm) <- anaProcTerm q gVars lVars 339 -- mfs is the fully qualified formula version of f 313 340 mfs <- anaFormulaCspCASL (gVars `Map.union` lVars) f 341 addDiags [mkDiag Debug "Formula" f] 342 addDiags [mkDiag Debug "FQFormula" (Maybe.fromJust mfs)] 314 343 let fComms = case mfs of 315 344 Nothing -> S.empty 316 345 Just fs -> formulaComms fs 317 return (S.unions [pComms, qComms, fComms]) 346 return (S.unions [pComms, qComms, fComms], 347 FQProcess (ConditionalProcess (Maybe.fromJust mfs) pFQTerm qFQTerm range) 348 (S.unions [pComms, qComms, fComms]) range) 318 349 319 350 -- | Statically analyse a CspCASL "named process" term. … … 582 613 ga = globAnnos sig 583 614 mix = emptyMix { mixRules = makeRules ga allIds } 584 resF <- resolveFormula (putParen mix) (mixResolve mix) 585 ga (mixRules mix) frm 615 resF <- resolveFormula (putParen mix) (mixResolve mix) ga (mixRules mix) frm 586 616 minExpFORMULA (const return) sig resF 587 617 -
trunk/CspCASL/Trans_Consts.hs
r10619 r11215 19 19 20 20 import CASL.AS_Basic_CASL 21 import CspCASL.AS_CspCASL_Process (PROCESS_NAME) 21 22 import Isabelle.IsaConsts 22 23 import Isabelle.IsaSign 24 import Isabelle.Translate(showIsaTypeT) 23 25 26 -- Name for the PreAlphabet 27 preAlphabetS :: String 28 preAlphabetS = "PreAlphabet" 29 30 -- Type for the PreAlphabet 31 preAlphabetType :: Typ 32 preAlphabetType = Type {typeId = preAlphabetS, 33 typeSort = [], 34 typeArgs =[]} 35 36 -- Name for the Alphabet 24 37 alphabetS :: String 25 38 alphabetS = "Alphabet" 26 39 40 -- Type for the Alphabet 41 alphabetType :: Typ 42 alphabetType = Type {typeId = alphabetS, 43 typeSort = [], 44 typeArgs =[]} 45 46 -- Name for IsabelleHOL quot type 47 quotS :: String 48 quotS = "quot" 49 50 -- Type for preAlphabet quot 51 preAlphabetQuotType :: Typ 52 preAlphabetQuotType = Type {typeId = quotS, 53 typeSort = [], 54 typeArgs =[preAlphabetType]} 55 56 -- Name for the datatype of process names 57 procNameS :: String 58 procNameS = "ProcName" 59 60 -- Type for the datatype of process names 61 procNameType :: Typ 62 procNameType = Type {typeId = procNameS, 63 typeSort = [], 64 typeArgs =[]} 65 66 -- name for CspProvers ('pn, 'a) proc type 67 procS :: String 68 procS = "proc" 69 70 -- Type for (ProcName,Alpahbet) proc 71 cCProverProcType :: Typ 72 cCProverProcType = Type {typeId = procS, 73 typeSort = [], 74 typeArgs =[procNameType, alphabetType]} 75 76 -- Name for the function for mapping process names to real processes 77 procMapS :: String 78 procMapS = "ProcMap" 79 80 -- Type for the function for mapping process names to real processes 81 procMapType :: Typ 82 procMapType = mkFunType procNameType cCProverProcType 83 27 84 barExtS :: String 28 85 barExtS = "_Bar" 86 87 baseSign :: BaseSig 88 baseSign = Main_thy 29 89 30 90 classS :: String … … 36 96 -- Convert a SORT to a string 37 97 convertSort2String :: SORT -> String 38 convertSort2String s = show s 98 convertSort2String s = showIsaTypeT s baseSign 99 100 convertProcessName2String :: PROCESS_NAME -> String 101 convertProcessName2String pn = (show pn) -
trunk/CspCASL/Trans_CspProver.hs
r10931 r11215 15 15 module CspCASL.Trans_CspProver where 16 16 17 import CASL.AS_Basic_CASL (SORT, VAR) 17 import qualified CASL.AS_Basic_CASL as CASL_AS_Basic_CASL 18 import qualified CASL.Fold as CASL_Fold 19 import qualified CASL.Sign as CASL_Sign 18 20 19 21 import Common.Id 22 23 import qualified Comorphisms.CFOL2IsabelleHOL as CFOL2IsabelleHOL 20 24 21 25 import CspCASL.AS_CspCASL_Process … … 26 30 import Isabelle.IsaConsts 27 31 28 transProcess :: PROCESS -> Term29 transProcess pr = case pr of32 transProcess :: CASL_Sign.Sign () () -> PROCESS -> Term 33 transProcess caslSign pr = case pr of 30 34 -- precedence 0 31 35 Skip _ -> cspProver_skipOp … … 41 45 -- precedence 1 42 46 ConditionalProcess _ p q _ -> 43 cspProver_conditionalOp true (transProcess p) (transProcess q) 47 cspProver_conditionalOp true (transProcess caslSign p) 48 (transProcess caslSign q) 44 49 -- precedence 2 45 50 Hiding p es _ -> 46 cspProver_hidingOp (transProcess p) (transEventSet es)51 cspProver_hidingOp (transProcess caslSign p) (transEventSet es) 47 52 RenamingProcess p r _ -> 48 cspProver_renamingOp (transProcess p) (transRenaming r)53 cspProver_renamingOp (transProcess caslSign p) (transRenaming r) 49 54 -- precedence 3 50 55 Sequential p q _ -> 51 cspProver_sequenceOp (transProcess p) (transProcessq)56 cspProver_sequenceOp (transProcess caslSign p) (transProcess caslSign q) 52 57 PrefixProcess ev p _ -> 53 cspProver_action_prefixOp (transEvent ev) (transProcess p) 58 cspProver_action_prefixOp (transEvent caslSign ev) 59 (transProcess caslSign p) 54 60 InternalPrefixProcess v s p _ -> 55 61 cspProver_internal_prefix_choiceOp (transVar v) 56 62 (transSort s) 57 (transProcess p)63 (transProcess caslSign p) 58 64 ExternalPrefixProcess v s p _ -> 59 65 cspProver_external_prefix_choiceOp (transVar v) 60 66 (transSort s) 61 (transProcess p)67 (transProcess caslSign p) 62 68 -- precedence 4 63 69 InternalChoice p q _ -> 64 cspProver_internal_choiceOp (transProcess p) (transProcess q) 70 cspProver_internal_choiceOp (transProcess caslSign p) 71 (transProcess caslSign q) 65 72 ExternalChoice p q _ -> 66 cspProver_external_choiceOp (transProcess p) (transProcess q) 73 cspProver_external_choiceOp (transProcess caslSign p) 74 (transProcess caslSign q) 67 75 -- precedence 5 68 76 Interleaving p q _ -> 69 cspProver_interleavingOp (transProcess p) (transProcess q) 77 cspProver_interleavingOp (transProcess caslSign p) 78 (transProcess caslSign q) 70 79 SynchronousParallel p q _ -> 71 cspProver_synchronousOp (transProcess p) (transProcess q) 80 cspProver_synchronousOp (transProcess caslSign p) 81 (transProcess caslSign q) 72 82 GeneralisedParallel p es q _ -> 73 cspProver_general_parallelOp (transProcess p)83 cspProver_general_parallelOp (transProcess caslSign p) 74 84 (transEventSet es) 75 (transProcess q)85 (transProcess caslSign q) 76 86 77 87 AlphabetisedParallel p les res q _ -> 78 cspProver_alphabetised_parallelOp (transProcess p)88 cspProver_alphabetised_parallelOp (transProcess caslSign p) 79 89 (transEventSet les) 80 90 (transEventSet res) 81 (transProcess q) 91 (transProcess caslSign q) 92 -- BUG not done right yet 93 FQProcess p _ _ -> 94 transProcess caslSign p 82 95 83 96 transEventSet :: EVENT_SET -> Term … … 88 101 EventSet commTypes _ -> Set $ FixedSet $ map tranCommType commTypes 89 102 90 transEvent :: EVENT -> Term91 transEvent ev =103 transEvent :: CASL_Sign.Sign () () -> EVENT -> Term 104 transEvent caslSign ev = 92 105 case ev of 93 TermEvent _caslTerm _ -> conDouble "not yet done"94 ChanSend _ _ _ -> conDouble " not yet done"95 ChanNonDetSend _ _ _ _ -> conDouble " not yet done"96 ChanRecv _ _ _ _ -> conDouble " not yet done"106 TermEvent caslTerm _ -> transTerm_with_class caslSign caslTerm 107 ChanSend _ _ _ -> conDouble "ChanSendNotYetDone" 108 ChanNonDetSend _ _ _ _ -> conDouble "ChanNonDetSendNotYetDone" 109 ChanRecv _ _ _ _ -> conDouble "ChanRecvNotYetDone" 97 110 98 transVar :: VAR -> Term111 transVar :: CASL_AS_Basic_CASL.VAR -> Term 99 112 transVar v = conDouble $ tokStr v 100 113 101 transSort :: SORT -> Term114 transSort :: CASL_AS_Basic_CASL.SORT -> Term 102 115 transSort sort = let sortBarString = convertSort2String sort ++ barExtS 103 116 in conDouble sortBarString … … 105 118 transRenaming :: RENAMING -> Term 106 119 transRenaming _ = conDouble "not yet done" 120 121 122 123 -- BUG - I dont think these functions are correct 124 transTerm_with_class :: CASL_Sign.Sign () () -> CASL_AS_Basic_CASL.TERM () -> 125 Term 126 transTerm_with_class caslSign caslTerm = 127 case caslTerm of 128 -- if the term is just a variable then we just translate the 129 -- variable to isabelle 130 CASL_AS_Basic_CASL.Qual_var _ _ _ -> transCaslTerm caslSign caslTerm 131 -- otherwise we add a classOp around it and translate the inside of 132 -- it with the translator that adds a chooseOp 133 _ -> classOp (transTerm_with_choose caslSign caslTerm) 134 135 transTerm_with_choose :: CASL_Sign.Sign () () -> CASL_AS_Basic_CASL.TERM () -> 136 Term 137 transTerm_with_choose caslSign caslTerm = 138 case caslTerm of 139 -- if the term is just a variable then we need to apply the choose 140 -- function 141 CASL_AS_Basic_CASL.Qual_var _ _ _ -> termAppl (conDouble "choose") 142 (transCaslTerm caslSign caslTerm) 143 -- otherwise we just translate it to Isabelle 144 _ -> transCaslTerm caslSign caslTerm 145 146 -- | Translate a CASL Term to an Isabelle Term using the exact 147 -- translation as is done in the comorphism composition 148 -- CASL2PCFOL;defaultCASL2SubCFOL;CFOL2IsabelleHOL 149 transCaslTerm :: CASL_Sign.Sign () () -> CASL_AS_Basic_CASL.TERM () -> Term 150 transCaslTerm caslSign caslTerm = 151 let tyToks = CFOL2IsabelleHOL.typeToks caslSign 152 trForm = CFOL2IsabelleHOL.formTrCASL 153 strs = CFOL2IsabelleHOL.getAssumpsToks caslSign 154 in CASL_Fold.foldTerm (CFOL2IsabelleHOL.transRecord 155 caslSign tyToks trForm strs) caslTerm 156 157 158 -- My own version of transRecord 159 -- transRecord_Term :: CASL.Sign.Sign f e -> Set.Set String -> FormulaTranslator f e 160 -- -> Set.Set String -> Record f Term Term 161 -- transRecord_Term sign tyToks tr toks = Record 162 -- { foldSimpleId = error "transRecord_Term: Simple_id" 163 -- , foldQual_var = \ _ v _ _ -> mkFree $ transVar toks v 164 -- , foldApplication = \ _ opsymb args _ -> 165 -- foldl termAppl (con $ transOP_SYMB sign tyToks opsymb) args 166 -- , foldSorted_term = \ _ t _ _ -> t -- no subsorting assumed 167 -- , foldCast = \ _ t _ _ -> t -- no subsorting assumed 168 -- , foldConditional = \ _ t1 phi t2 _ -> -- equal types assumed 169 -- If phi t1 t2 NotCont 170 -- , foldMixfix_qual_pred = error "transRecord_Term: Mixfix_qual_pred" 171 -- , foldMixfix_term = error "transRecord_Term: Mixfix_term" 172 -- , foldMixfix_token = error "transRecord_Term: Mixfix_token" 173 -- , foldMixfix_sorted_term = error "transRecord_Term: Mixfix_sorted_term" 174 -- , foldMixfix_cast = error "transRecord_Term: Mixfix_cast" 175 -- , foldMixfix_parenthesized = error "transRecord_Term: Mixfix_parenthesized" 176 -- , foldMixfix_bracketed = error "transRecord_Term: Mixfix_bracketed" 177 -- , foldMixfix_braced = error "transRecord_Term: Mixfix_braced" 178 -- } 179 180 -- transVar :: Set.Set String -> VAR -> String 181 -- transVar toks v = let 182 -- s = showIsaConstT (simpleIdToId v) baseSign 183 -- renVar t = if Set.member t toks then renVar $ "X_" ++ t else t 184 -- in renVar s 185
