Normalize formulas

diff --git a/Connections.hs b/Connections.hs
index 1361ea6a3313775807dc45cd59eb4888fbc95a00..e6a5267de621b7f30f16fc8af17f760ce7444c8a 100644 (file)
--- a/Connections.hs
+++ b/Connections.hs
@@ -205,6 +205,11 @@ dnf (phi :/\: psi) =
                         | a <- Set.toList (dnf phi)
                         , b <- Set.toList (dnf psi) ]
 
+fromDNF :: Set (Set (Name,Dir)) -> Formula
+fromDNF s = foldr orFormula (Dir Zero) (map (foldr andFormula (Dir One)) fs)
+  where xss = map Set.toList $ Set.toList s
+        fs = [ [ if d == Zero then NegAtom n else Atom n | (n,d) <- xs ] | xs <- xss ]
+
 merge :: Set (Set (Name,Dir)) -> Set (Set (Name,Dir)) -> Set (Set (Name,Dir))
 merge a b =
   let as = Set.toList a
@@ -212,12 +217,6 @@ merge a 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

diff --git a/Eval.hs b/Eval.hs
index c42632979e8f7a0e8819204ec3d9087a47a333f4..882c58c33db3e65aec2e00a4d092472a4e951830 100644 (file)
--- a/Eval.hs
+++ b/Eval.hs
@@ -814,12 +814,15 @@ instance Normal Val where
     VSnd t              -> sndVal (normal ns t)
     VSplit u t          -> VSplit (normal ns u) (normal ns t)
     VApp u v            -> app (normal ns u) (normal ns v)
-    VAppFormula u phi   -> VAppFormula (normal ns u) phi
+    VAppFormula u phi   -> VAppFormula (normal ns u) (normal ns phi)
     _                   -> v
 
 instance Normal Env where
   normal ns = mapEnv (normal ns) id
 
+instance Normal Formula where
+  normal _ = fromDNF . dnf
+
 instance Normal a => Normal (Map k a) where
   normal ns us = Map.map (normal ns) us