From: Anders <mortberg@chalmers.se>
Date: Fri, 27 Mar 2015 16:52:26 +0000 (+0100)
Subject: Fix conversion of formulas
X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=665712a06e00f1e5b45aadc5224cf8a875c15179;p=cubicaltt.git

Fix conversion of formulas
---

diff --git a/Connections.hs b/Connections.hs
index c36d5c5..e5c4565 100644
--- a/Connections.hs
+++ b/Connections.hs
@@ -194,6 +194,16 @@ orFormula (Dir Zero) phi = phi
 orFormula phi (Dir Zero) = phi
 orFormula phi psi        = phi :\/: psi
 
+dnf :: Formula -> Set (Set (Name,Dir))
+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) ]
+
 -- evalFormula :: Formula -> Face -> Formula
 -- evalFormula phi alpha =
 --   Map.foldWithKey (\i d psi -> act psi (i,Dir d)) phi alpha
diff --git a/Eval.hs b/Eval.hs
index 35c3801..fccd22e 100644
--- a/Eval.hs
+++ b/Eval.hs
@@ -753,4 +753,4 @@ instance Convertible a => Convertible (System a) where
                   and (elems (intersectionWith (conv k) ts ts'))
 
 instance Convertible Formula where
-  conv _ phi psi = sort (invFormula phi 1) == sort (invFormula psi 1)
+  conv _ phi psi = dnf phi == dnf psi