From: Anders 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