Changeset 12732

Timestamp:

26.10.2009 17:31:19 (4 weeks ago)

Author:

codruta

Message:

Changed ExtModal/Logic?_ExtModal.hs

Location:

trunk

Files:

• Comorphisms/LogicList.hs (modified) (2 diffs)
• ExtModal/ExtModalSign.hs (modified) (1 diff)
• ExtModal/ExtModalSystems.hs (modified) (2 diffs)
• ExtModal/Logic_ExtModal.hs (modified) (8 diffs)
• ExtModal/MorphismExtension.hs (modified) (3 diffs)
• ExtModal/Parse_AS.hs (modified) (1 diff)

trunk/Comorphisms/LogicList.hs

@@ -50 +50 @@
 #ifdef CASLEXTENSIONS
 import Modal.Logic_Modal
+import ExtModal.Logic_ExtModal
 import CoCASL.Logic_CoCASL
 import CspCASL.Logic_CspCASL
@@ -80 +81 @@
 #ifdef CASLEXTENSIONS
   , Logic CoCASL
+  , Logic ExtModal
   , Logic Modal
   , Logic cspCASL

trunk/ExtModal/ExtModalSign.hs

@@ -14 +14 @@
 
 import CASL.Sign
+
 import Common.Id
+import Common.DocUtils
+import Common.Doc
 
 import qualified Data.Map as Map

trunk/ExtModal/ExtModalSystems.hs

@@ -1 +1 @@
 {-to generate by utils genTransMFormFunc.pl -}
 
-module Modal.ModalSystems  where
+module ExtModal.ExtModalSystems  where
 
 import Common.DocUtils
@@ -12 +12 @@
 -- ExtModal
 import ExtModal.AS_ExtModal
-import ExtModal.Print_AS ()
+import ExtModal.Print_AS
 

trunk/ExtModal/Logic_ExtModal.hs

@@ -17 +17 @@
 import ExtModal.ATC_ExtModal()
 import ExtModal.Parse_AS
+import ExtModal.Print_AS
 import ExtModal.StatAna
 import ExtModal.MorphismExtension
 
+import CASL.Formula
 import CASL.Sign
 import CASL.Morphism
@@ -29 +31 @@
 import CASL.SymbolParser
 import CASL.Sublogic
+import CASL.SimplifySen
+import CASL.Taxonomy
 import CASL.Logic_CASL ()
 import Logic.Logic
@@ -58 +62 @@
 
 -- Modal formula mapping via signature morphism
-map_EM_FORMULA :: MapSen EM_FORMULA EModalSign (DefMorExt EModalSign)
+map_EM_FORMULA :: MapSen EM_FORMULA EModalSign MorphExtension
 
 map_EM_FORMULA morph (BoxOrDiamond choice t_m leq_geq number f pos) = 
@@ -73 +77 @@
 
 
-map_EM_FORMULA morph (Hybrid choice nom f pos) = 
-        let new_nom = let nms = nom_map (extended_map morph) in
-                        if Map.member nom nms then (nms Map.! nom) else nom
-            new_f = mapSen map_EM_FORMULA morph f
-        in Hybrid choice new_nom new_f pos
+map_EM_FORMULA morph (Hybrid choice nm f pos) =
+        let new_nom = case nm of 
+                        Nominal nom -> let nms = nom_map (extended_map morph) 
+                                       in if Map.member nom nms then (Nominal (nms Map.! nom)) else nm
+                        _ -> nm
+            new_f = mapSen map_EM_FORMULA morph f
+        in Hybrid choice new_nom new_f pos
+                
 
 map_EM_FORMULA morph (UntilSince choice f1 f2 pos) = 
@@ -94 +101 @@
 map_EM_FORMULA morph (StateQuantification t_dir choice f pos) = 
         let new_f = mapSen map_EM_FORMULA morph f
-        in StatQuantification t_dir choice new_f pos
+        in StateQuantification t_dir choice new_f pos
 
 map_EM_FORMULA morph (FixedPoint choice p_var f pos) = 
@@ -103 +110 @@
 simEMSen :: Sign EM_FORMULA EModalSign -> EM_FORMULA -> EM_FORMULA
 simEMSen sign (BoxOrDiamond choice tm leq_geq number f pos) = 
-        BoxOrDiamond choice tm leq_geq number (simplifySen minExpForm simEMSen sign f) pos
+        BoxOrDiamond choice tm leq_geq number (simplifySen frmTypeAna simEMSen sign f) pos
 simEMSen sign (Hybrid choice nom f pos) = 
-        Hybrid choice nom (simplifySen minExpForm simEMSen sign f) pos
+        Hybrid choice nom (simplifySen frmTypeAna simEMSen sign f) pos
 simEMSen sign (UntilSince choice f1 f2 pos) = 
-        UntilSince choice (simplifySen minExpForm simEMSen sign f1) 
-                (simplifySen minExpForm simEMSen sign f1) pos
+        UntilSince choice (simplifySen frmTypeAna simEMSen sign f1) 
+                (simplifySen frmTypeAna simEMSen sign f1) pos
 simEMSen sign (NextY choice f pos) =
-        NextY choice (simplifySen minExpForm simEMSen sign f) pos
+        NextY choice (simplifySen frmTypeAna simEMSen sign f) pos
 simEMSen sign (PathQuantification choice f pos) = 
-        PathQuantification choice (simplifySen minExpForm simEMSen sign f) pos
+        PathQuantification choice (simplifySen frmTypeAna simEMSen sign f) pos
 simEMSen sign (StateQuantification t_dir choice f pos) = 
-        StateQuantification t_dir choice (simplifySen minExpForm simEMSen sign f) pos
+        StateQuantification t_dir choice (simplifySen frmTypeAna simEMSen sign f) pos
 simEMSen sign (FixedPoint choice p_var f pos) = 
-        FixedPoint choice p_var (simplifySen minExpForm simEMSen sign f) pos
+        FixedPoint choice p_var (simplifySen frmTypeAna simEMSen sign f) pos
 
 instance Sentences ExtModal ExtModalFORMULA ExtModalSign ExtModalMorph Symbol where 
         map_sen ExtModal morph = return . mapSen map_EM_FORMULA morph
-        simplify_sen ExtModal = simplifySen minExpForm simEMSen
-        parse_sentence ExtModal = Just modalFormulaParser
+        simplify_sen ExtModal = simplifySen frmTypeAna simEMSen
+        parse_sentence ExtModal = Just $ primFormula ext_modal_reserved_words
         print_sign ExtModal sig = printSign 
-                (printEModalSign $ simplifySen minExpForm simEMSen sig) sig
+                (printEModalSign $ simplifySen frmTypeAna simEMSen sig) sig
         sym_of ExtModal = symOf 
         symmap_of ExtModal = morphismToSymbMap
@@ -129 +136 @@
 
 instance StaticAnalysis ExtModal EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS 
-                ExtModalSign ExtModalMorph Symbol RawSymbol () where 
+                ExtModalSign ExtModalMorph Symbol RawSymbol where 
         basic_analysis ExtModal = Just basicEModalAnalysis
         stat_symb_map_items ExtModal = statSymbMapItems
@@ -152 +159 @@
         theory_to_taxonomy ExtModal = convTaxo
 
-instance Logic () EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS 
+instance Logic ExtModal () EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS 
                 ExtModalSign ExtModalMorph Symbol RawSymbol () where 
 

trunk/ExtModal/MorphismExtension.hs

@@ -18 +18 @@
 import Common.Id
 import Common.Result
+import Common.DocUtils
+import Common.Doc
 
 import ExtModal.AS_ExtModal
 import ExtModal.ExtModalSign
+import ExtModal.Print_AS
 
 data MorphExtension = MorphExtension
-        { source :: Sign EM_FORMULA EModalSign
-        , target :: Sign EM_FORMULA EModalSign
+        { source :: EModalSign
+        , target :: EModalSign
         , mod_map :: Map.Map SIMPLE_ID SIMPLE_ID
         , nom_map :: Map.Map SIMPLE_ID SIMPLE_ID
@@ -30 +33 @@
 
 emptyMorphExtension :: MorphExtension 
-emptyMorphExtension = MorphExtension (emptySign emptyEModalSign) (emptySign emptyEModalSign) Map.empty Map.empty
+emptyMorphExtension = MorphExtension emptyEModalSign emptyEModalSign Map.empty Map.empty
 
-instance MorphismExtension (Sign EM_FORMULA EModalSign) MorphExtension where 
+
+instance Pretty MorphExtension where 
+        pretty me = pretty (source me) <+> pretty (target me) <+> 
+                        text (show (Map.toList (mod_map me))) <+> text (show (Map.toList (nom_map me)))
+
+instance MorphismExtension EModalSign MorphExtension where 
  
         ideMorphismExtension sgn = 
                 let insert_next old_map s_id = Map.insert  s_id s_id old_map in
                 MorphExtension sgn sgn 
-                        (foldl insert_next Map.empty (Map.keys (modalities (extendedInfo sgn)))) 
-                        (foldl insert_next Map.empty (Set.toList (nominals (extendedInfo sgn))))
+                        (foldl insert_next Map.empty (Map.keys (modalities sgn)))
+                        (foldl insert_next Map.empty (Set.toList (nominals sgn)))
 
         composeMorphismExtension sgn me1 me2 = 
@@ -57 +65 @@
                     occurs_alt ((me_k,me_val1):l) False me_val2 = 
                         if me_val1 == me_val2 then occurs_alt l True me_val2 else occurs_alt l False me_val2
-                in if Map.keys (modalities (extendedInfo (target me))) == Map.elems (mod_map me) 
-                        && Set.toList (nominals (extendedInfo (target me))) == Map.elems (nom_map me)
+                in if Map.keys (modalities (target me)) == Map.elems (mod_map me) 
+                        && Set.toList (nominals (target me)) == Map.elems (nom_map me)
                         && Map.filter (occurs_alt (Map.toList (mod_map me)) False) (mod_map me) == Map.empty
                         && Map.filter (occurs_alt (Map.toList (nom_map me)) False) (nom_map me) == Map.empty 

trunk/ExtModal/Parse_AS.hs

@@ -188 +188 @@
 
 {-Term modality parser-}
--- parseModality :: [String] -> AParser st MODALITY
 parseModality :: GenParser Char (AnnoState st) MODALITY
 parseModality =