Comments and cleanup

yav · Oct 5, 2013 · 2fae34f · 2fae34f
1 parent ac14052
commit 2fae34f
Show file tree

Hide file tree

Showing 2 changed files with 18 additions and 17 deletions.
diff --git a/src/Data/Integer/Presburger.hs b/src/Data/Integer/Presburger.hs
@@ -172,14 +172,16 @@ nat x = 0 |<=| x
 
 --------------------------------------------------------------------------------
 isTrue :: Formula -> Bool
-isTrue (F _ fo) = case A.isBool =<< A.isFAtom fo of
-                    Just x -> x
-                    Nothing
-                     | Just (c, f1, f2) <- A.isFConn fo
-                       -> case c of
-                            A.And -> isTrue (F undefined f1) && isTrue (F undefined f2)
-                            A.Or  -> isTrue (F undefined f1) || isTrue (F undefined f2)
-                    _  -> error "Unexpected free variables in term"
+isTrue (F _ fo0) = go fo0
+  where
+  go fo = case A.isBool =<< A.isFAtom fo of
+            Just x -> x
+            Nothing ->
+              case A.isFConn fo of
+                Just (c, f1, f2) -> case c of
+                                      A.And -> go f1 && go f2
+                                      A.Or  -> go f1 || go f2
+                _  -> error "Unexpected free variables in term"
 
 
 

diff --git a/src/Data/Integer/Presburger/Formula.hs b/src/Data/Integer/Presburger/Formula.hs
@@ -79,17 +79,16 @@ fConns c fs   = foldr1 (fConn c) fs
 
 fConn :: Conn -> Formula -> Formula -> Formula
 
-fConn And f1@(AtomF (Bool False)) _                        = f1
-fConn And    (AtomF (Bool True))  f2                       = f2
--- fConn And _                       f2@(AtomF (Bool False))  = f2
--- fConn And f1                         (AtomF (Bool True))   = f1
+-- NOTE: Here we only simply True/False when it appears in the first argument.
+-- This memory leaks where we have to fullly evaluate both sub-formulas
+-- before we know the top-most connective in the formula.
+fConn And f1@(AtomF (Bool False)) _   = f1
+fConn And    (AtomF (Bool True))  f2  = f2
 
-fConn Or  f1@(AtomF (Bool True))  _                        = f1
-fConn Or     (AtomF (Bool False)) f2                       = f2
--- fConn Or  _                       f2@(AtomF (Bool True))   = f2
--- fConn Or  f1                         (AtomF (Bool False))  = f1
+fConn Or  f1@(AtomF (Bool True))  _   = f1
+fConn Or     (AtomF (Bool False)) f2  = f2
 
-fConn c f1 f2 = ConnF c f1 f2
+fConn c f1 f2                         = ConnF c f1 f2
 
 fAtom :: Atom -> Formula
 fAtom = AtomF