Started the implementation of simplify_sen for CASL and corrected its…

… type signature git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@3092 cec4b9c1-7d33-0410-9eda-942365e851bb
spechub · Aug 26, 2004 · 59cc761 · 59cc761
1 parent bc96650
commit 59cc761
Show file tree

Hide file tree

Showing 3 changed files with 11 additions and 3 deletions.
diff --git a/CASL/Logic_CASL.hs b/CASL/Logic_CASL.hs
@@ -58,6 +58,13 @@ dummy _ _ = ()
 trueC :: a -> b -> Bool
 trueC _ _ = True
 
+--     simplify_sen :: lid -> sign -> sentence -> sentence
+simplifySen :: (Sign f e -> a -> a) -> Sign f e -> FORMULA a -> FORMULA a
+simplifySen e_func sign form = 
+    case form of
+    ExtFORMULA f -> ExtFORMULA $ e_func sign f
+    _ -> form
+
 -- Typeable instance
 tc_BASIC_SPEC, tc_SYMB_ITEMS, tc_SYMB_MAP_ITEMS, casl_SublocigsTc,
              sentenceTc, signTc, morphismTc, symbolTc, rawSymbolTc :: TyCon
@@ -147,6 +154,7 @@ instance Sentences CASL CASLFORMULA () CASLSign CASLMor Symbol where
       symmap_of CASL = morphismToSymbMap
       sym_name CASL = symName
       consCheck CASL = checkFreeType
+      simplify_sen CASL = simplifySen dummy
 
 instance StaticAnalysis CASL CASLBasicSpec CASLFORMULA ()
                SYMB_ITEMS SYMB_MAP_ITEMS

diff --git a/Logic/Grothendieck.hs b/Logic/Grothendieck.hs
@@ -198,7 +198,7 @@ sublogicOfTh (G_theory lid sigma sens) =
 -- | simplify a theory (throw away qualifications)
 simplifyTh :: G_theory -> G_theory
 simplifyTh (G_theory lid sigma sens) =
-  G_theory lid sigma (map (mapNamed (simplify_sen lid)) sens)
+  G_theory lid sigma (map (mapNamed (simplify_sen lid sigma)) sens)
 
 -- | Grothendieck symbols
 data G_symbol = forall lid sublogics

diff --git a/Logic/Logic.hs b/Logic/Logic.hs
@@ -160,8 +160,8 @@ class (Category lid sign morphism, Ord sentence,
          -- sentence translation
       map_sen :: lid -> morphism -> sentence -> Result sentence
          -- simplification of sentences (leave out qualifications)
-      simplify_sen :: lid -> sentence -> sentence
-      simplify_sen _ = id  -- default implementation
+      simplify_sen :: lid -> sign -> sentence -> sentence
+      simplify_sen _ _ = id  -- default implementation
          -- parsing of sentences
       parse_sentence :: lid -> Maybe (sign -> String -> Result sentence)
            -- is a term parser needed as well?