From: Anders <mortberg@chalmers.se>
Date: Thu, 23 Apr 2015 15:26:18 +0000 (+0200)
Subject: Normalize formulas
X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=53de597039d06c8b8f13dc8baaa9819173b8651c;p=cubicaltt.git

Normalize formulas
---

diff --git a/Connections.hs b/Connections.hs
index 1361ea6..e6a5267 100644
--- 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 c426329..882c58c 100644
--- 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