Changeset 12793

Timestamp:

06.11.2009 16:57:28 (2 weeks ago)

Author:

maeder

Message:

corrected symmetry axioms

Files:

• trunk/Comorphisms/CASL2TopSort.hs (modified) (2 diffs)

trunk/Comorphisms/CASL2TopSort.hs

@@ -217 +217 @@
 symmetryAxioms ssMap sortRels =
     let symSets = Rel.sccOfClosure sortRels
-        mR = Rel.mostRight sortRels
-        symTopSorts = not . Set.null . Set.intersection mR
-        toAxioms symSet = map (\ s ->
+        toAxioms symSet = concatMap
+          (\ s ->
             let ts = lkupTop ssMap s
                 Just symS = lkupPredName ssMap s
@@ -225 +224 @@
                 vd = mkVarDeclStr "x" ts
                 vt = toQualVar vd
-            in makeNamed (show ts ++ "_symmetric_with_" ++ show symS)
-                   $ mkForall [vd] (Predication psy [vt] nullRange) nullRange
-            ) $ Set.toList (Set.difference symSet mR)
-    in concatMap toAxioms (filter symTopSorts symSets)
+            in if ts == s then [] else
+                   [makeNamed (show ts ++ "_symmetric_with_" ++ show symS)
+                   $ mkForall [vd] (Predication psy [vt] nullRange) nullRange]
+          ) $ Set.toList symSet
+    in concatMap toAxioms symSets
 
 generateAxioms :: SubSortMap -> Map.Map PRED_NAME (Set.Set PredType)