Fix dnf

diff --git a/Connections.hs b/Connections.hs
index 3e3c34b8299bac80768f7a40ff9673803fb48c8e..1361ea6a3313775807dc45cd59eb4888fbc95a00 100644 (file)
--- a/Connections.hs
+++ b/Connections.hs
@@ -199,11 +199,25 @@ dnf (Dir One)      = Set.singleton Set.empty
 dnf (Dir Zero)     = Set.empty
 dnf (Atom n)       = Set.singleton (Set.singleton (n,1))
 dnf (NegAtom n)    = Set.singleton (Set.singleton (n,0))
-dnf (phi :\/: psi) = dnf phi `Set.union` dnf psi
-dnf (phi :/\: psi) = Set.fromList [ a `Set.union` b
-                                  | a <- Set.toList (dnf phi)
-                                  , b <- Set.toList (dnf psi) ]
-
+dnf (phi :\/: psi) = dnf phi `merge` dnf psi
+dnf (phi :/\: psi) =
+  foldr merge Set.empty [ Set.singleton (a `Set.union` b)
+                        | a <- Set.toList (dnf phi)
+                        , b <- Set.toList (dnf psi) ]
+
+merge :: Set (Set (Name,Dir)) -> Set (Set (Name,Dir)) -> Set (Set (Name,Dir))
+merge a b =
+  let as = Set.toList a
+      bs = Set.toList b
+  in Set.fromList [ ai | ai <- as, not (any (\bj -> bj `Set.isProperSubsetOf` ai) bs) ] `Set.union`
+     Set.fromList [ bi | bi <- bs, not (any (\aj -> aj `Set.isProperSubsetOf` bi) as) ] 
+
+
+i = Atom (Name "i")
+j = Atom (Name "j")
+nj = NegAtom (Name "j")
+phi = i :\/: nj :\/: (i :/\: j)
+psi = (i :/\: j) :\/: (i :/\: j)
 -- evalFormula :: Formula -> Face -> Formula
 -- evalFormula phi alpha =
 --   Map.foldWithKey (\i d psi -> act psi (i,Dir d)) phi alpha