From: Anders <mortberg@chalmers.se>
Date: Thu, 23 Apr 2015 15:04:11 +0000 (+0200)
Subject: Fix dnf
X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=27e825fa09715cfdb37a3f92b816d51415b70f21;p=cubicaltt.git

Fix dnf
---

diff --git a/Connections.hs b/Connections.hs
index 3e3c34b..1361ea6 100644
--- 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