Changeset 12736
- Timestamp:
- 27.10.2009 10:37:15 (4 weeks ago)
- Location:
- trunk/ExtModal
- Files:
-
- 5 modified
-
ExtModalSign.hs (modified) (1 diff)
-
MorphismExtension.hs (modified) (4 diffs)
-
Parse_AS.hs (modified) (7 diffs)
-
Print_AS.hs (modified) (5 diffs)
-
StatAna.hs (modified) (2 diffs)
Legend:
- Unmodified
- Added
- Removed
-
trunk/ExtModal/ExtModalSign.hs
r12732 r12736 16 16 17 17 import Common.Id 18 import Common.DocUtils19 import Common.Doc20 18 21 19 import qualified Data.Map as Map -
trunk/ExtModal/MorphismExtension.hs
r12732 r12736 14 14 import qualified Data.Set as Set 15 15 16 import CASL.Sign17 16 import CASL.Morphism 18 17 import Common.Id 19 import Common.Result20 import Common.DocUtils21 import Common.Doc22 18 23 import ExtModal.AS_ExtModal24 19 import ExtModal.ExtModalSign 25 import ExtModal.Print_AS26 20 27 21 data MorphExtension = MorphExtension … … 36 30 37 31 38 instance Pretty MorphExtension where39 pretty me = pretty (source me) <+> pretty (target me) <+>40 text (show (Map.toList (mod_map me))) <+> text (show (Map.toList (nom_map me)))41 42 32 instance MorphismExtension EModalSign MorphExtension where 43 33 … … 48 38 (foldl insert_next Map.empty (Set.toList (nominals sgn))) 49 39 50 composeMorphismExtension sgnme1 me2 =40 composeMorphismExtension _ me1 me2 = 51 41 if me1 == me2 52 42 then let me_compos second_map old_map (me_k, me_val) = … … 60 50 inverseMorphismExtension me = 61 51 let swap_arrows old_map (me_k, me_val) = Map.insert me_val me_k old_map 62 occurs_alt [] once me_val= once63 occurs_alt (( me_k,me_val1):l) True me_val2 =52 occurs_alt [] once _ = once 53 occurs_alt ((_,me_val1):l) True me_val2 = 64 54 if me_val1 == me_val2 then True else occurs_alt l True me_val2 65 occurs_alt (( me_k,me_val1):l) False me_val2 =55 occurs_alt ((_,me_val1):l) False me_val2 = 66 56 if me_val1 == me_val2 then occurs_alt l True me_val2 else occurs_alt l False me_val2 67 57 in if Map.keys (modalities (target me)) == Map.elems (mod_map me) -
trunk/ExtModal/Parse_AS.hs
r12732 r12736 48 48 modal <- parseModality 49 49 close <- cBracketT 50 grading <-asKey lessEq51 number <- getNumber 52 formula <- primFormula ext_modal_reserved_words53 return (BoxOrDiamond True modal True (value 10 number) formula $ toRange open [] close)50 asKey lessEq 51 number <- getNumber 52 em_formula <- primFormula ext_modal_reserved_words 53 return (BoxOrDiamond True modal True (value 10 number) em_formula $ toRange open [] close) 54 54 <|> 55 55 {-box, >=-} … … 57 57 modal <- parseModality 58 58 close <- cBracketT 59 grading <-asKey greaterEq60 number <- getNumber 61 formula <- primFormula ext_modal_reserved_words62 return (BoxOrDiamond True modal False (value 10 number) formula $ toRange open [] close)59 asKey greaterEq 60 number <- getNumber 61 em_formula <- primFormula ext_modal_reserved_words 62 return (BoxOrDiamond True modal False (value 10 number) em_formula $ toRange open [] close) 63 63 <|> 64 64 {-diamond, <=-} … … 66 66 modal <- parseModality 67 67 close <- asKey greaterS 68 grading <-asKey lessEq69 number <- getNumber 70 formula <- primFormula ext_modal_reserved_words71 return (BoxOrDiamond False modal True (value 10 number) formula $ toRange open [] close)68 asKey lessEq 69 number <- getNumber 70 em_formula <- primFormula ext_modal_reserved_words 71 return (BoxOrDiamond False modal True (value 10 number) em_formula $ toRange open [] close) 72 72 <|> 73 73 {-diamond, >=-} … … 75 75 modal <- parseModality 76 76 close <- asKey greaterS 77 grading <-asKey greaterEq78 number <- getNumber 79 formula <- primFormula ext_modal_reserved_words80 return (BoxOrDiamond False modal False (value 10 number) formula $ toRange open [] close)77 asKey greaterEq 78 number <- getNumber 79 em_formula <- primFormula ext_modal_reserved_words 80 return (BoxOrDiamond False modal False (value 10 number) em_formula $ toRange open [] close) 81 81 <|> 82 82 {-empty diamond, <=-} 83 83 do diam <- asKey diamondS 84 grading <-asKey lessEq85 number <- getNumber 86 formula <- primFormula ext_modal_reserved_words84 asKey lessEq 85 number <- getNumber 86 em_formula <- primFormula ext_modal_reserved_words 87 87 let pos = tokPos diam 88 return (BoxOrDiamond False (Simple_modality $ Token emptyS pos) True (value 10 number) formula pos)88 return (BoxOrDiamond False (Simple_modality $ Token emptyS pos) True (value 10 number) em_formula pos) 89 89 <|> 90 90 {-empty diamond, >=-} 91 91 do diam <- asKey diamondS 92 grading <-asKey greaterEq93 number <- getNumber 94 formula <- primFormula ext_modal_reserved_words92 asKey greaterEq 93 number <- getNumber 94 em_formula <- primFormula ext_modal_reserved_words 95 95 let pos = tokPos diam 96 return (BoxOrDiamond False (Simple_modality $ Token emptyS pos) False (value 10 number) formula pos)96 return (BoxOrDiamond False (Simple_modality $ Token emptyS pos) False (value 10 number) em_formula pos) 97 97 <|> 98 98 {-Until, U-} … … 112 112 {-All paths, A-} 113 113 do ap <- asKey allPathsS 114 formula <- primFormula ext_modal_reserved_words114 em_formula <- primFormula ext_modal_reserved_words 115 115 let pos = tokPos ap 116 return (PathQuantification True formula pos)116 return (PathQuantification True em_formula pos) 117 117 <|> 118 118 {-Some paths, E-} 119 119 do sp <- asKey somePathsS 120 formula <- primFormula ext_modal_reserved_words120 em_formula <- primFormula ext_modal_reserved_words 121 121 let pos = tokPos sp 122 return (PathQuantification False formula pos)122 return (PathQuantification False em_formula pos) 123 123 <|> 124 124 {-Next, X-} 125 125 do nxt <- asKey nextS 126 formula <- primFormula ext_modal_reserved_words126 em_formula <- primFormula ext_modal_reserved_words 127 127 let pos = tokPos nxt 128 return (NextY True formula pos)128 return (NextY True em_formula pos) 129 129 <|> 130 130 {-Yesterday, Y-} 131 131 do ysd <- asKey yesterdayS 132 formula <- primFormula ext_modal_reserved_words132 em_formula <- primFormula ext_modal_reserved_words 133 133 let pos = tokPos ysd 134 return (NextY False formula pos)134 return (NextY False em_formula pos) 135 135 <|> 136 136 {-Generally, G-} 137 137 do grl <- asKey generallyS 138 formula <- primFormula ext_modal_reserved_words138 em_formula <- primFormula ext_modal_reserved_words 139 139 let pos = tokPos grl 140 return (StateQuantification True True formula pos)140 return (StateQuantification True True em_formula pos) 141 141 <|> 142 142 {-Eventually, F-} 143 143 do evt <- asKey eventuallyS 144 formula <- primFormula ext_modal_reserved_words144 em_formula <- primFormula ext_modal_reserved_words 145 145 let pos = tokPos evt 146 return (StateQuantification True False formula pos)146 return (StateQuantification True False em_formula pos) 147 147 <|> 148 148 {-Hitherto, H-} 149 149 do hth <- asKey hithertoS 150 formula <- primFormula ext_modal_reserved_words150 em_formula <- primFormula ext_modal_reserved_words 151 151 let pos = tokPos hth 152 return (StateQuantification False True formula pos)152 return (StateQuantification False True em_formula pos) 153 153 <|> 154 154 {-Previously, P-} 155 155 do prv <- asKey previouslyS 156 formula <- primFormula ext_modal_reserved_words156 em_formula <- primFormula ext_modal_reserved_words 157 157 let pos = tokPos prv 158 return (StateQuantification False False formula pos)158 return (StateQuantification False False em_formula pos) 159 159 <|> 160 160 {-parse Mu-} 161 161 do mu <- asKey muS 162 162 z <- varId ext_modal_reserved_words 163 formula <- primFormula ext_modal_reserved_words163 em_formula <- primFormula ext_modal_reserved_words 164 164 let pos = tokPos mu 165 return (FixedPoint True z formula pos)165 return (FixedPoint True z em_formula pos) 166 166 <|> 167 167 {-parse Nu-} 168 168 do nu <- asKey nuS 169 169 z <- varId ext_modal_reserved_words 170 formula <- primFormula ext_modal_reserved_words170 em_formula <- primFormula ext_modal_reserved_words 171 171 let pos = tokPos nu 172 return (FixedPoint False z formula pos)172 return (FixedPoint False z em_formula pos) 173 173 <|> 174 174 {-@-} 175 175 do at <- asKey atS 176 176 nom <- simpleId 177 formula <- primFormula ext_modal_reserved_words177 em_formula <- primFormula ext_modal_reserved_words 178 178 let pos = tokPos at 179 return (Hybrid True (Nominal nom) formula pos)179 return (Hybrid True (Nominal nom) em_formula pos) 180 180 <|> 181 181 {-Here-} 182 182 do her <- asKey hereS 183 183 nom <- simpleId 184 formula <- primFormula ext_modal_reserved_words184 em_formula <- primFormula ext_modal_reserved_words 185 185 let pos = tokPos her 186 return (Hybrid False (Nominal nom) formula pos)186 return (Hybrid False (Nominal nom) em_formula pos) 187 187 188 188 … … 193 193 return (Simple_modality t) 194 194 <|> 195 do opn <-asKey tmOParanthS195 do asKey tmOParanthS 196 196 t <- parseModality 197 cls <-asKey tmCParanthS197 asKey tmCParanthS 198 198 return t 199 199 <|> 200 200 do f <- primFormula ext_modal_reserved_words 201 grd <-asKey tmGuardS201 asKey tmGuardS 202 202 return (Guard f) 203 203 <|> 204 204 do t <- parseModality 205 tc <-asKey tmTransClosS205 asKey tmTransClosS 206 206 return (TransitiveClosure t) 207 207 <|> 208 208 do t1 <- parseModality 209 cmp <-asKey tmCompositionS209 asKey tmCompositionS 210 210 t2 <- parseModality 211 211 return (Composition t1 t2) 212 212 <|> 213 213 do t1 <- parseModality 214 un <-asKey tmUnionS214 asKey tmUnionS 215 215 t2 <- parseModality 216 216 return (Union t1 t2) … … 249 249 parseAxioms False annoId ( catRange $ k : ks ) 250 250 <|> 251 do tmp <-asKey timeS251 do asKey timeS 252 252 k <- mKey 253 253 (annoId, ks) <- separatedBy (annoParser simpleId) anComma -
trunk/ExtModal/Print_AS.hs
r12645 r12736 13 13 module ExtModal.Print_AS where 14 14 15 import Common.Id16 15 import Common.Keywords 17 16 import qualified Data.Map as Map … … 24 23 import ExtModal.ExtModalSign 25 24 import ExtModal.Keywords 25 import ExtModal.MorphismExtension 26 26 27 27 import CASL.AS_Basic_CASL (FORMULA(..)) … … 62 62 63 63 instance Pretty EM_FORMULA where 64 pretty (BoxOrDiamond choice modality leq_geq number sentence _) =64 pretty (BoxOrDiamond choice modality leq_geq number em_sentence _) = 65 65 let sp = case modality of 66 66 Simple_modality _ -> (<>) … … 69 69 in sep $ (if choice then brackets mdl else less `sp` mdl `sp` greater) 70 70 : (if leq_geq then keyword lessEq else keyword greaterEq) 71 : (text (show number)) : space : [condParensInnerF (printFormula pretty) parens sentence]71 : (text (show number)) : space : [condParensInnerF (printFormula pretty) parens em_sentence] 72 72 73 pretty (Hybrid choice nom sentence _) =73 pretty (Hybrid choice nom em_sentence _) = 74 74 sep $ (if choice then keyword atS else keyword hereS) : space : (pretty nom) : space 75 : [condParensInnerF (printFormula pretty) parens sentence]75 : [condParensInnerF (printFormula pretty) parens em_sentence] 76 76 pretty (UntilSince choice sentence1 sentence2 _) = 77 77 sep $ ([condParensInnerF (printFormula pretty) parens sentence1] 78 78 ++ ( space : (if choice then keyword untilS else keyword sinceS) : space 79 79 : [condParensInnerF (printFormula pretty) parens sentence2])) 80 pretty (PathQuantification choice sentence _) =80 pretty (PathQuantification choice em_sentence _) = 81 81 sep $ (if choice then keyword allPathsS else keyword somePathsS) : space 82 : [condParensInnerF (printFormula pretty) parens sentence]83 pretty (NextY choice sentence _) =82 : [condParensInnerF (printFormula pretty) parens em_sentence] 83 pretty (NextY choice em_sentence _) = 84 84 sep $ (if choice then keyword nextS else keyword yesterdayS) : space 85 : [condParensInnerF (printFormula pretty) parens sentence]86 pretty (StateQuantification dir_choice choice sentence _) =85 : [condParensInnerF (printFormula pretty) parens em_sentence] 86 pretty (StateQuantification dir_choice choice em_sentence _) = 87 87 let kw = case dir_choice of 88 88 True -> if choice then keyword generallyS else keyword eventuallyS 89 89 _ -> if choice then keyword hithertoS else keyword previouslyS 90 in sep $ kw : space : [condParensInnerF (printFormula pretty) parens sentence] 90 in sep $ kw : space : [condParensInnerF (printFormula pretty) parens em_sentence] 91 pretty (FixedPoint choice p_var em_sentence _) = 92 sep $ (if choice then keyword muS else keyword nuS) : space : (pretty p_var) : space 93 : [condParensInnerF (printFormula pretty) parens em_sentence] 91 94 92 95 condParensInnerF :: Pretty f => (FORMULA f -> Doc) -> (Doc -> Doc) -> FORMULA f -> Doc … … 132 135 vcat . map (\ tf -> fsep $ punctuate semi $ map (printAnnoted $ pretty . sim) tf) 133 136 137 instance Pretty MorphExtension where 138 pretty me = pretty (source me) <+> pretty (target me) <+> 139 text (show (Map.toList (mod_map me))) <+> text (show (Map.toList (nom_map me))) 140 -
trunk/ExtModal/StatAna.hs
r12674 r12736 43 43 freeVarsOfExt sign ( StateQuantification _ _ f _ ) = freeVars sign f 44 44 freeVarsOfExt sign ( NextY _ f _ ) = freeVars sign f 45 freeVarsOfExt sign ( FixedPoint _ fpvarf _ ) = freeVars sign f45 freeVarsOfExt sign ( FixedPoint _ _ f _ ) = freeVars sign f 46 46 47 47 basicEModalAnalysis … … 68 68 Union md1 md2 -> do new_md1 <- checkMod md1 69 69 new_md2 <- checkMod md2 70 return $ Union md1md270 return $ Union new_md1 new_md2 71 71 TransitiveClosure md -> do new_md <- checkMod md 72 72 return $ TransitiveClosure new_md
