Changeset 11215 for trunk/Comorphisms/CspCASL2IsabelleHOL.hs
- Timestamp:
- 05.01.2009 15:46:06 (11 months ago)
- Files:
-
- 1 modified
-
trunk/Comorphisms/CspCASL2IsabelleHOL.hs (modified) (19 diffs)
Legend:
- Unmodified
- Added
- Removed
-
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
