Changeset 12726

Timestamp:

26.10.2009 16:00:16 (4 weeks ago)

Author:

mcodescu

Message:

made an algorithm generic to reuse it for OWL

Location:

trunk

Files:

• CASL/ColimSign.hs (modified) (3 diffs)
• Common/SetColimit.hs (modified) (3 diffs)
• Propositional/Analysis.hs (modified) (2 diffs)

trunk/CASL/ColimSign.hs

@@ -15 +15 @@
 -}
 
-module CASL.ColimSign(signColimit, extCASLColimit, renameSorts) where
+module CASL.ColimSign(signColimit, extCASLColimit) where
 
 import CASL.Sign
@@ -57 +57 @@
    sortGraph = emap getSortMap $ nmap sortSet graph
    (setSort0, funSort0) = computeColimitSet sortGraph
-   (setSort, funSort) = renameSorts (setSort0, funSort0)
+   (setSort, funSort) = addIntToSymbols (setSort0, funSort0)
    sigmaSort = (emptySign $ error "err"){sortSet=setSort}
    phiSort = Map.fromList
@@ -80 +80 @@
      phiAssoc
    in (sigmaExt, phiExt)
-
--- method for adding the number as suffix of the id it pairs
-addSuffixToId :: (Id, Node) -> Id
-addSuffixToId (idN, n) = appendNumber idN n
-
---method for applying the renaming to the colimit of sorts
-renameSorts :: (Set.Set (Id, Node), Map.Map Node (Map.Map Id (Id, Node))) ->
-               (Set.Set Id, Map.Map Node (EndoMap Id))
-renameSorts (set, fun) = let
-  fstEqual (x1,_) (x2,_) = x1 == x2
-  partList pairSet = leqClasses fstEqual pairSet
-  namePartitions elemList f0 s1 f1 = case elemList of
-   [] -> (s1, f1)
-   p:ps -> if length p == 1 then
-     -- a single element with this name,it can be kept
-    let s2 = Set.insert (fst $ head p) s1
-        updateF node = Map.union (Map.findWithDefault (error "f1") node f1) $
-                       Map.fromList $ map (\x -> (x, fst $ head p)) $
-                       filter (\x -> Map.findWithDefault (error "fo(node)") x
-                                      (Map.findWithDefault (error "f0") node f0)
-                                     == head p) $
-                       Map.keys $ Map.findWithDefault (error "f0")
-                                   node f0
-        f2 = Map.fromList $ zip (Map.keys f0) $ map updateF $ Map.keys f0
-    in namePartitions ps f0 s2 f2
-                else
-     --several elements with same name, the number is added at the end
-    let s2 = Set.union s1 $ Set.fromList $ map addSuffixToId p
-        updateF node = Map.union (Map.findWithDefault (error "f1") node f1) $
-             Map.fromList $
-             map ( \x -> (x, addSuffixToId $
-                                  Map.findWithDefault (error "addSuffixToId") x
-                                  (Map.findWithDefault (error "f0") node f0))) $
-             filter (\x -> (Map.findWithDefault (error "fo(node)") x
-                           (Map.findWithDefault (error "f0") node f0))
-                           `elem` p) $
-             Map.keys $ Map.findWithDefault (error "f0") node f0
-        f2 = Map.fromList $ zip (Map.keys f0) $ map updateF $ Map.keys f0
-    in namePartitions ps f0 s2 f2
- in namePartitions (partList set) fun (Set.empty) $
-    Map.fromList $ zip (Map.keys fun) (repeat Map.empty)
 
 -- computing subsorts in the colimit

trunk/Common/SetColimit.hs

@@ -18 +18 @@
 
 module Common.SetColimit(
-    computeColimitSet
+    computeColimitSet,
+    addIntToSymbols
   )
  where
@@ -27 +28 @@
 import qualified Data.Set as Set
 import Data.List
+import CASL.Overload(leqClasses)
+import Common.Id
 
 compose :: (Ord a) => Set.Set (a, Int) ->
@@ -102 +105 @@
     in computeCoeqs graph (colim', morMap') edges'
 
+class (Eq a, Ord a) => SymbolName a where
+  addIntAsSuffix :: (a, Int) -> a
+
+instance SymbolName Id where
+ addIntAsSuffix (x,y) = appendNumber x y
+
+addIntToSymbols :: (SymbolName a) =>
+               (Set.Set (a, Node), Map.Map Node (Map.Map a (a, Node))) ->
+               (Set.Set a, Map.Map Node (Map.Map a a))
+addIntToSymbols (set, fun) = let
+  fstEqual (x1,_) (x2,_) = x1 == x2
+  partList pairSet = leqClasses fstEqual pairSet
+  namePartitions elemList f0 s1 f1 = case elemList of
+   [] -> (s1, f1)
+   p:ps -> if length p == 1 then
+     -- a single element with this name,it can be kept
+    let s2 = Set.insert (fst $ head p) s1
+        updateF node = Map.union (Map.findWithDefault (error "f1") node f1) $
+                       Map.fromList $ map (\x -> (x, fst $ head p)) $
+                       filter (\x -> Map.findWithDefault (error "fo(node)") x
+                                      (Map.findWithDefault (error "f0") node f0)
+                                     == head p) $
+                       Map.keys $ Map.findWithDefault (error "f0")
+                                   node f0
+        f2 = Map.fromList $ zip (Map.keys f0) $ map updateF $ Map.keys f0
+    in namePartitions ps f0 s2 f2
+                else
+     --several elements with same name, the number is added at the end
+    let s2 = Set.union s1 $ Set.fromList $ map addIntAsSuffix p
+        updateF node = Map.union (Map.findWithDefault (error "f1") node f1) $
+             Map.fromList $
+             map ( \x -> (x, addIntAsSuffix $
+                                  Map.findWithDefault (error "addSuffixToId") x
+                                  (Map.findWithDefault (error "f0") node f0))) $
+             filter (\x -> (Map.findWithDefault (error "fo(node)") x
+                           (Map.findWithDefault (error "f0") node f0))
+                           `elem` p) $
+             Map.keys $ Map.findWithDefault (error "f0") node f0
+        f2 = Map.fromList $ zip (Map.keys f0) $ map updateF $ Map.keys f0
+    in namePartitions ps f0 s2 f2
+ in namePartitions (partList set) fun (Set.empty) $
+    Map.fromList $ zip (Map.keys fun) (repeat Map.empty)
 
 
-

trunk/Propositional/Analysis.hs

@@ -43 +43 @@
 import Data.Graph.Inductive.Graph
 import Common.SetColimit
-import CASL.ColimSign(renameSorts)
 
 -- | Datatype for formulas with diagnosis data
@@ -393 +392 @@
 signatureColimit graph = do
  let graph1 = nmap Sign.items $ emap (\(x,y) -> (x, Morphism.propMap y)) graph
-     (set, maps) = renameSorts $ computeColimitSet graph1
+     (set, maps) = addIntToSymbols $ computeColimitSet graph1
      cSig = Sign.Sign{Sign.items = set}
  return (cSig,