refactored the G_symbolplmap to more generic types 'Map a symbol' and…

… 'Map symbol a'

git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@13278 cec4b9c1-7d33-0410-9eda-942365e851bb

ATC/Grothendieck.der.hs

@@ -126,18 +126,32 @@ instance ShATermLG G_symbol where
                 (att2, G_symbol lid i2') }}}
             u -> fromShATermError "G_symbol" u
 
-instance ShATermLG G_symbolplmap where
-  toShATermLG att0 (G_symbolplmap lid m) = do
+instance (Ord a, ShATermLG a) => ShATermLG (G_symbolmap a) where
+  toShATermLG att0 (G_symbolmap lid m) = do
          (att1,i1) <- toShATermLG' att0 (language_name lid)
          (att2,i2) <- toShATermLG' att1 m
-         return $ addATerm (ShAAppl "G_symbolplmap" [i1,i2] []) att2
+         return $ addATerm (ShAAppl "G_symbolmap" [i1,i2] []) att2
   fromShATermLG lg ix att = case getShATerm ix att of
-            ShAAppl "G_symbolplmap" [i1,i2] _ ->
+            ShAAppl "G_symbolmap" [i1,i2] _ ->
                 case fromShATermLG' lg i1 att of { (att1, i1') ->
-                case atcLogicLookup lg "G_symbolplmap" i1' of { Logic lid ->
+                case atcLogicLookup lg "G_symbolmap" i1' of { Logic lid ->
                 case fromShATermLG' lg i2 att1 of { (att2, i2') ->
-                (att2, G_symbolplmap lid i2') }}}
-            u -> fromShATermError "G_symbolplmap" u
+                (att2, G_symbolmap lid i2') }}}
+            u -> fromShATermError "G_symbolmap" u
+
+instance (Ord a, ShATermLG a) => ShATermLG (G_mapofsymbol a) where
+  toShATermLG att0 (G_mapofsymbol lid m) = do
+         (att1,i1) <- toShATermLG' att0 (language_name lid)
+         (att2,i2) <- toShATermLG' att1 m
+         return $ addATerm (ShAAppl "G_mapofsymbol" [i1,i2] []) att2
+  fromShATermLG lg ix att = case getShATerm ix att of
+            ShAAppl "G_mapofsymbol" [i1,i2] _ ->
+                case fromShATermLG' lg i1 att of { (att1, i1') ->
+                case atcLogicLookup lg "G_mapofsymbol" i1' of { Logic lid ->
+                case fromShATermLG' lg i2 att1 of { (att2, i2') ->
+                (att2, G_mapofsymbol lid i2') }}}
+            u -> fromShATermError "G_mapofsymbol" u
+
 
 instance ShATermLG G_symb_items_list where
   toShATermLG att0 (G_symb_items_list lid symb_items) = do

Logic/Coerce.hs

@@ -17,7 +17,6 @@ import Logic.Logic
 import Logic.Prover
 import Common.ExtSign
 import Common.Id
-import Common.LibName
 import Common.Result
 import Common.AS_Annotation
 import qualified Data.Set as Set
@@ -113,15 +112,25 @@ coerceSymbol ::
    => lid1 -> lid2 -> symbol1 -> symbol2
 coerceSymbol l1 l2 s1 = unsafeCoerce l1 l2 s1
 
-coerceSymbolplmap ::
+coerceSymbolmap ::
    (Logic  lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
                 sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
    Logic  lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
                 sign2 morphism2 symbol2 raw_symbol2 proof_tree2,
    Typeable a)
-   => lid1 -> lid2 -> Map.Map symbol1 [LinkPath a]
-           -> Map.Map symbol2 [LinkPath a]
-coerceSymbolplmap l1 l2 sm1 = unsafeCoerce l1 l2 sm1
+   => lid1 -> lid2 -> Map.Map symbol1 a
+           -> Map.Map symbol2 a
+coerceSymbolmap l1 l2 sm1 = unsafeCoerce l1 l2 sm1
+
+coerceMapofsymbol ::
+   (Logic  lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
+                sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
+   Logic  lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
+                sign2 morphism2 symbol2 raw_symbol2 proof_tree2,
+   Typeable a)
+   => lid1 -> lid2 -> Map.Map a symbol1
+           -> Map.Map a symbol2
+coerceMapofsymbol l1 l2 sm1 = unsafeCoerce l1 l2 sm1
 
 coerceSymbItemsList ::
   (Logic  lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1

Logic/Grothendieck.hs

@@ -43,7 +43,8 @@ module Logic.Grothendieck
   , isHomSubGsign
   , isSubGsign
   , langNameSig
-  , G_symbolplmap (..)
+  , G_symbolmap (..)
+  , G_mapofsymbol (..)
   , G_symbol (..)
   , G_symb_items_list (..)
   , G_symb_map_items_list (..)
@@ -103,7 +104,6 @@ import Common.Doc
 import Common.DocUtils
 import Common.ExtSign
 import Common.Id
-import Common.LibName
 import Common.Lexer
 import Common.Parsec
 import Common.Result
@@ -206,28 +206,52 @@ instance Pretty G_sign where
 langNameSig :: G_sign -> String
 langNameSig (G_sign lid _ _) = language_name lid
 
+-- | Grothendieck maps with symbol as keys
+data G_symbolmap a = forall lid sublogics
+        basic_spec sentence symb_items symb_map_items
+         sign morphism symbol raw_symbol proof_tree .
+        Logic lid sublogics
+         basic_spec sentence symb_items symb_map_items
+          sign morphism symbol raw_symbol proof_tree  =>
+  G_symbolmap lid (Map.Map symbol a)
+  deriving Typeable
+
+instance Show a => Show (G_symbolmap a) where
+    show (G_symbolmap _ sm) = show sm
 
-data G_symbolplmap = forall lid sublogics
+instance (Typeable a, Ord a) => Eq (G_symbolmap a) where
+    a == b = compare a b == EQ
+
+instance (Typeable a, Ord a) => Ord (G_symbolmap a) where
+  compare (G_symbolmap l1 sm1) (G_symbolmap l2 sm2) =
+    case compare (language_name l1) $ language_name l2 of
+      EQ -> compare (coerceSymbolmap l1 l2 sm1) sm2
+      r -> r
+
+
+-- | Grothendieck maps with symbol as values
+data G_mapofsymbol a = forall lid sublogics
         basic_spec sentence symb_items symb_map_items
          sign morphism symbol raw_symbol proof_tree .
         Logic lid sublogics
          basic_spec sentence symb_items symb_map_items
           sign morphism symbol raw_symbol proof_tree  =>
-  G_symbolplmap lid (Map.Map symbol [SLinkPath])
+  G_mapofsymbol lid (Map.Map a symbol)
   deriving Typeable
 
-instance Show G_symbolplmap where
-    show (G_symbolplmap _ sm) = show sm
+instance Show a => Show (G_mapofsymbol a) where
+    show (G_mapofsymbol _ sm) = show sm
 
-instance Eq G_symbolplmap where
+instance (Typeable a, Ord a) => Eq (G_mapofsymbol a) where
     a == b = compare a b == EQ
 
-instance Ord G_symbolplmap where
-  compare (G_symbolplmap l1 sm1) (G_symbolplmap l2 sm2) =
+instance (Typeable a, Ord a) => Ord (G_mapofsymbol a) where
+  compare (G_mapofsymbol l1 sm1) (G_mapofsymbol l2 sm2) =
     case compare (language_name l1) $ language_name l2 of
-      EQ -> compare (coerceSymbolplmap l1 l2 sm1) sm2
+      EQ -> compare (coerceMapofsymbol l1 l2 sm1) sm2
       r -> r
 
+
 -- | Grothendieck symbols
 data G_symbol = forall lid sublogics
         basic_spec sentence symb_items symb_map_items

Logic/Logic.hs

@@ -134,12 +134,15 @@ import Common.Item
 import qualified Data.Set as Set
 import qualified Data.Map as Map
 import Data.Typeable
+import Control.Monad (unless)
 
 import qualified OMDoc.DataTypes as OMDoc ( TCElement
                                           , TCorOMElement
                                           , NameMap
                                           , SigMap
-                                          , OMCD)
+                                          , SigMapI
+                                          , OMCD
+                                          , OmdADT)
 
 
 -- | Stability of logic implementations
@@ -400,6 +403,9 @@ class ( Syntax lid basic_spec symb_items symb_map_items
          --------------- operations on signatures and morphisms -----------
          -- | the empty (initial) signature, see CASL RefMan p. 193
          empty_signature :: lid -> sign
+         -- | adds a symbol to a given signature
+         add_symb_to_sign :: lid -> sign -> symbol -> Result sign
+         add_symb_to_sign l _ _ = statFail l "add_symb_to_sign"
          -- | union of signatures, see CASL RefMan p. 193
          signature_union :: lid -> sign -> sign -> Result sign
          signature_union l _ _ = statFail l "signature_union"
@@ -587,28 +593,60 @@ class (StaticAnalysis lid
          empty_proof_tree l = statError l "empty_proof_tree"
 
          ----------------------- OMDoc ---------------------------
+
+         omdoc_metatheory :: lid -> Maybe OMDoc.OMCD
+         -- default implementation, no logic should throw an error here
+         -- and the base of omcd should be a parseable URI
+         omdoc_metatheory _lid = Nothing
+
+
          export_symToOmdoc :: lid -> OMDoc.NameMap symbol
                            -> symbol -> String -> Result OMDoc.TCElement
-         -- default implementation
-         export_symToOmdoc l _ _ = statError l "export_symToOmdoc"
+         export_symToOmdoc l _ _ = statFail l "export_symToOmdoc"
 
          export_senToOmdoc :: lid -> OMDoc.NameMap symbol
                           -> sentence -> Result OMDoc.TCorOMElement
-         -- default implementation
-         export_senToOmdoc l _ _  = statError l "export_senToOmdoc"
+         export_senToOmdoc l _ _  = statFail l "export_senToOmdoc"
 
-         -- | additional information which have to be exported can be
+         -- | additional information which has to be exported can be
          --   exported by this function
          export_theoryToOmdoc :: lid -> OMDoc.SigMap symbol -> sign
                               -> [Named sentence] -> Result [OMDoc.TCElement]
          -- default implementation does no extra export
          -- , sufficient in some cases
          export_theoryToOmdoc _ _ _ _  = return []
 
-         omdoc_metatheory :: lid -> Maybe OMDoc.OMCD
-         -- default implementation, no logic should throw an error here
-         -- and the base of omcd should be a parseable URI
-         omdoc_metatheory _lid = Nothing
+
+         omdocToSym :: lid -> OMDoc.SigMapI symbol -> OMDoc.TCElement
+                    -> String -> Result symbol
+         omdocToSym l _ _ _ = statFail l "omdocToSym"
+
+         omdocToSen :: lid -> OMDoc.SigMapI symbol -> OMDoc.TCElement
+                    -> String -> Result (Maybe (Named sentence))
+         omdocToSen l _ _ _ = statFail l "omdocToSen"
+
+         -- | abstract datatypes are imported with this function.
+         --   By default the input is returned without changes.
+         addOMadtToTheory :: lid -> OMDoc.SigMapI symbol
+                          -> (sign, [Named sentence]) -> [[OMDoc.OmdADT]]
+                          -> Result (sign, [Named sentence])
+         -- no logic should throw an error here
+         addOMadtToTheory l _ t adts = do
+           unless (null adts) $ warning ()
+                      (concat [ "ADT handling not implemented for logic "
+                              , show l, " but some adts have to be handled" ])
+                      nullRange
+           return t
+
+         -- | additional information which has to be imported can be
+         --   imported by this function. By default the input is returned
+         --   without changes.
+         addOmdocToTheory :: lid -> OMDoc.SigMapI symbol
+                          -> (sign, [Named sentence]) -> [OMDoc.TCElement]
+                          -> Result (sign, [Named sentence])
+         -- no logic should throw an error here
+         addOmdocToTheory _ _ t _ = return t
+
 
 ----------------------------------------------------------------
 -- Derived functions

Proofs/PathifyNames.hs

@@ -71,7 +71,7 @@ pathifyLabNode le li dg (n, lb) =
       -- get the global imports
       innMorphs <- getGlobalImports lid dg $ innDG dg n
       m <- pathifySign lid li sig innMorphs
-      let nlb = lb { dgn_symbolpathlist = G_symbolplmap lid m }
+      let nlb = lb { dgn_symbolpathlist = G_symbolmap lid m }
       return $ changesDGH dg [SetNodeLab lb (n, nlb)]
 
 
@@ -124,22 +124,22 @@ getGlobalImport lid dg (from, _, llab) =
                     hmor <- coerceMorphism (targetLogic cid) lid
                             "getGlobalImport" mor
                     case dgn_symbolpathlist $ labDG dg from of
-                      G_symbolplmap lid0 m ->
+                      G_symbolmap lid0 m ->
                           if isIdComorphism (Comorphism cid)
                           then
                           return $ Just (n, hmor, isHidingDef lt
-                                        , coerceSymbolplmap lid0 lid m)
+                                        , coerceSymbolmap lid0 lid m)
                           else
                               do
                                 warning () ("translating by comorphism "
                                             ++ show cid) nullRange
                                 let plmap = Map.mapKeys
                                              (sglElem (show cid)
                                               . map_symbol cid sign1)
-                                             $ coerceSymbolplmap lid0
+                                             $ coerceSymbolmap lid0
                                                   (sourceLogic cid) m
                                 return $ Just (n, hmor, isHidingDef lt,
-                                                coerceSymbolplmap
+                                                coerceSymbolmap
                                                 (targetLogic cid) lid plmap)
     -- theorem links will be skipped
     else return Nothing

Static/DevGraph.hs

@@ -165,7 +165,7 @@ data DGNodeLab =
   , dgn_phi :: Maybe GMorphism --morphism from signature to nffree signature
   , nodeInfo :: DGNodeInfo
   , dgn_lock :: Maybe (MVar ())
-  , dgn_symbolpathlist :: G_symbolplmap
+  , dgn_symbolpathlist :: G_symbolmap [SLinkPath]
   } deriving (Show, Eq)
 
 instance Show (MVar a) where
@@ -728,7 +728,7 @@ newInfoNodeLab name info gTh@(G_theory lid _ _ _ _) = DGNodeLab
   , dgn_phi = Nothing
   , nodeInfo = info
   , dgn_lock = Nothing
-  , dgn_symbolpathlist = G_symbolplmap lid Map.empty }
+  , dgn_symbolpathlist = G_symbolmap lid Map.empty }
 
 -- | create a new node label using 'newNodeInfo' and 'newInfoNodeLab'
 newNodeLab :: NodeName -> DGOrigin -> G_theory -> DGNodeLab