From 2fae34f4ce6dd287f423e691851c3c58fe31c84e Mon Sep 17 00:00:00 2001
From: "Iavor S. Diatchki" <iavor.diatchki@gmail.com>
Date: Sat, 5 Oct 2013 13:46:42 -0700
Subject: [PATCH] Comments and cleanup

---
 src/Data/Integer/Presburger.hs         | 18 ++++++++++--------
 src/Data/Integer/Presburger/Formula.hs | 17 ++++++++---------
 2 files changed, 18 insertions(+), 17 deletions(-)

diff --git a/src/Data/Integer/Presburger.hs b/src/Data/Integer/Presburger.hs
index 0719161..3eac6b9 100644
--- 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
index a5a7045..22eeca8 100644
--- 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