Changeset 12733
- Timestamp:
- 26.10.2009 17:55:50 (4 weeks ago)
- Location:
- trunk
- Files:
-
- 2 modified
-
ExtModal/Logic_ExtModal.hs (modified) (8 diffs)
-
Makefile (modified) (1 diff)
Legend:
- Unmodified
- Added
- Removed
-
trunk/ExtModal/Logic_ExtModal.hs
r12732 r12733 2 2 Module : ./ExtModal/Logic_ExtModal.hs 3 3 Description : Instance of class Logic for ExtModal 4 Copyright : 4 Copyright : 5 5 License : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt 6 6 Maintainer : codruta.liliana@gmail.com 7 7 Stability : experimental 8 Portability : 8 Portability : 9 9 10 10 Instance of class Logic for ExtModal … … 40 40 data ExtModal = ExtModal deriving Show 41 41 42 instance Language ExtModal where 42 instance Language ExtModal where 43 43 description _ = unlines 44 44 [ "ExtModal is the 'extended modal logic' extension of CASL. " … … 49 49 ] 50 50 51 type ExtModalSign = Sign EM_FORMULA EModalSign 51 type ExtModalSign = Sign EM_FORMULA EModalSign 52 52 type ExtModalMorph = Morphism EM_FORMULA EModalSign MorphExtension 53 53 type ExtModalFORMULA = FORMULA EM_FORMULA 54 54 55 instance SignExtension E xtModalSign where55 instance SignExtension EModalSign where 56 56 isSubSignExtension = isSubEModalSign 57 57 58 instance Syntax ExtModal EM_BASIC_SPEC SYMB_ITEMS SYMB_MAP_ITEMS where 58 instance Syntax ExtModal EM_BASIC_SPEC SYMB_ITEMS SYMB_MAP_ITEMS where 59 59 parse_basic_spec ExtModal = Just $ basicSpec ext_modal_reserved_words 60 60 parse_symb_items ExtModal = Just $ symbItems ext_modal_reserved_words … … 64 64 map_EM_FORMULA :: MapSen EM_FORMULA EModalSign MorphExtension 65 65 66 map_EM_FORMULA morph (BoxOrDiamond choice t_m leq_geq number f pos) = 67 let new_tm tm = case tm of 68 Simple_modality sm -> 66 map_EM_FORMULA morph (BoxOrDiamond choice t_m leq_geq number f pos) = 67 let new_tm tm = case tm of 68 Simple_modality sm -> 69 69 let mds = mod_map (extended_map morph) in 70 70 if Map.member sm mds then Simple_modality (mds Map.! sm) else tm … … 78 78 79 79 map_EM_FORMULA morph (Hybrid choice nm f pos) = 80 let new_nom = case nm of 81 Nominal nom -> let nms = nom_map (extended_map morph) 80 let new_nom = case nm of 81 Nominal nom -> let nms = nom_map (extended_map morph) 82 82 in if Map.member nom nms then (Nominal (nms Map.! nom)) else nm 83 83 _ -> nm 84 84 new_f = mapSen map_EM_FORMULA morph f 85 85 in Hybrid choice new_nom new_f pos 86 87 86 88 map_EM_FORMULA morph (UntilSince choice f1 f2 pos) = 87 88 map_EM_FORMULA morph (UntilSince choice f1 f2 pos) = 89 89 let new_f1 = mapSen map_EM_FORMULA morph f1 90 90 new_f2 = mapSen map_EM_FORMULA morph f2 91 91 in UntilSince choice new_f1 new_f2 pos 92 92 93 map_EM_FORMULA morph (NextY choice f pos) = 93 map_EM_FORMULA morph (NextY choice f pos) = 94 94 let new_f = mapSen map_EM_FORMULA morph f 95 95 in NextY choice new_f pos 96 96 97 map_EM_FORMULA morph (PathQuantification choice f pos) = 97 map_EM_FORMULA morph (PathQuantification choice f pos) = 98 98 let new_f = mapSen map_EM_FORMULA morph f 99 99 in PathQuantification choice new_f pos 100 100 101 map_EM_FORMULA morph (StateQuantification t_dir choice f pos) = 101 map_EM_FORMULA morph (StateQuantification t_dir choice f pos) = 102 102 let new_f = mapSen map_EM_FORMULA morph f 103 103 in StateQuantification t_dir choice new_f pos 104 104 105 map_EM_FORMULA morph (FixedPoint choice p_var f pos) = 105 map_EM_FORMULA morph (FixedPoint choice p_var f pos) = 106 106 let new_f = mapSen map_EM_FORMULA morph f 107 107 in FixedPoint choice p_var new_f pos … … 109 109 -- Simplification of formulas - simplifySen for ExtFORMULA 110 110 simEMSen :: Sign EM_FORMULA EModalSign -> EM_FORMULA -> EM_FORMULA 111 simEMSen sign (BoxOrDiamond choice tm leq_geq number f pos) = 111 simEMSen sign (BoxOrDiamond choice tm leq_geq number f pos) = 112 112 BoxOrDiamond choice tm leq_geq number (simplifySen frmTypeAna simEMSen sign f) pos 113 simEMSen sign (Hybrid choice nom f pos) = 113 simEMSen sign (Hybrid choice nom f pos) = 114 114 Hybrid choice nom (simplifySen frmTypeAna simEMSen sign f) pos 115 simEMSen sign (UntilSince choice f1 f2 pos) = 116 UntilSince choice (simplifySen frmTypeAna simEMSen sign f1) 115 simEMSen sign (UntilSince choice f1 f2 pos) = 116 UntilSince choice (simplifySen frmTypeAna simEMSen sign f1) 117 117 (simplifySen frmTypeAna simEMSen sign f1) pos 118 118 simEMSen sign (NextY choice f pos) = 119 119 NextY choice (simplifySen frmTypeAna simEMSen sign f) pos 120 simEMSen sign (PathQuantification choice f pos) = 120 simEMSen sign (PathQuantification choice f pos) = 121 121 PathQuantification choice (simplifySen frmTypeAna simEMSen sign f) pos 122 simEMSen sign (StateQuantification t_dir choice f pos) = 122 simEMSen sign (StateQuantification t_dir choice f pos) = 123 123 StateQuantification t_dir choice (simplifySen frmTypeAna simEMSen sign f) pos 124 simEMSen sign (FixedPoint choice p_var f pos) = 124 simEMSen sign (FixedPoint choice p_var f pos) = 125 125 FixedPoint choice p_var (simplifySen frmTypeAna simEMSen sign f) pos 126 126 127 instance Sentences ExtModal ExtModalFORMULA ExtModalSign ExtModalMorph Symbol where 127 instance Sentences ExtModal ExtModalFORMULA ExtModalSign ExtModalMorph Symbol where 128 128 map_sen ExtModal morph = return . mapSen map_EM_FORMULA morph 129 129 simplify_sen ExtModal = simplifySen frmTypeAna simEMSen 130 130 parse_sentence ExtModal = Just $ primFormula ext_modal_reserved_words 131 print_sign ExtModal sig = printSign 131 print_sign ExtModal sig = printSign 132 132 (printEModalSign $ simplifySen frmTypeAna simEMSen sig) sig 133 sym_of ExtModal = symOf 133 sym_of ExtModal = symOf 134 134 symmap_of ExtModal = morphismToSymbMap 135 135 sym_name ExtModal = symName 136 136 137 instance StaticAnalysis ExtModal EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS 138 ExtModalSign ExtModalMorph Symbol RawSymbol where 137 instance StaticAnalysis ExtModal EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS 138 ExtModalSign ExtModalMorph Symbol RawSymbol where 139 139 basic_analysis ExtModal = Just basicEModalAnalysis 140 140 stat_symb_map_items ExtModal = statSymbMapItems … … 144 144 id_to_raw ExtModal = idToRaw 145 145 matches ExtModal = CASL.Morphism.matches 146 146 147 147 empty_signature ExtModal = emptySign emptyEModalSign 148 148 signature_union ExtModal sgn = return . addSig addEModalSign sgn 149 intersection ExtModal sgn = return . interSig interEModalSign sgn 150 final_union ExtModal = finalUnion addEModalSign 149 intersection ExtModal sgn = return . interSig interEModalSign sgn 150 final_union ExtModal = finalUnion addEModalSign 151 151 morphism_union ExtModal = morphismUnion (const id) addEModalSign 152 152 is_subsig ExtModal = isSubSig isSubEModalSign … … 154 154 generated_sign ExtModal = generatedSign emptyMorphExtension 155 155 cogenerated_sign ExtModal = cogeneratedSign emptyMorphExtension 156 induced_from_morphism ExtModal = inducedFromMorphism emptyMorphExtension 157 induced_from_to_morphism ExtModal = 156 induced_from_morphism ExtModal = inducedFromMorphism emptyMorphExtension 157 induced_from_to_morphism ExtModal = 158 158 inducedFromToMorphism emptyMorphExtension isSubEModalSign diffEModalSign 159 159 theory_to_taxonomy ExtModal = convTaxo 160 160 161 instance Logic ExtModal () EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS 162 ExtModalSign ExtModalMorph Symbol RawSymbol () where 161 instance Logic ExtModal () EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS 162 ExtModalSign ExtModalMorph Symbol RawSymbol () where 163 163 164 stability _ = Experimental 165 empty_proof_tree _ = () 164 stability _ = Experimental 165 empty_proof_tree _ = () 166 166 -
trunk/Makefile
r12718 r12733 289 289 Maude/Symbol.hs Maude/AS_Maude.hs 290 290 291 ExtModal_files = ExtModal/AS_ExtModal.hs ExtModal/ExtModalSign.hs 291 ExtModal_files = ExtModal/AS_ExtModal.hs ExtModal/ExtModalSign.hs \ 292 ExtModal/MorphismExtension.hs 292 293 293 294 # ATC DrIFT-rule generation for logics
