From 04f75d9189f606d11a1a4edc85e791cb96bad14b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Facundo=20Dom=C3=ADnguez?= <facundo.dominguez@tweag.io>
Date: Fri, 13 May 2022 12:40:29 -0300
Subject: [PATCH] Add back bindings in pretty printing of environments

---
 src/Language/Fixpoint/Solver/Prettify.hs | 13 ++++++++++---
 1 file changed, 10 insertions(+), 3 deletions(-)

diff --git a/src/Language/Fixpoint/Solver/Prettify.hs b/src/Language/Fixpoint/Solver/Prettify.hs
index 305112d04..d674d1113 100644
--- a/src/Language/Fixpoint/Solver/Prettify.hs
+++ b/src/Language/Fixpoint/Solver/Prettify.hs
@@ -1,5 +1,6 @@
 {-# LANGUAGE LambdaCase #-}
 {-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE PatternSynonyms            #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 
 {-# OPTIONS_GHC -Wno-name-shadowing #-}
@@ -40,9 +41,11 @@ import           Language.Fixpoint.Types.Names
 import           Language.Fixpoint.Types.PrettyPrint
 import           Language.Fixpoint.Types.Refinements
   ( Expr(..)
+  , pattern PFalse
   , Reft
   , SortedReft(..)
   , conjuncts
+  , expr
   , reft
   , reftBind
   , reftPred
@@ -84,14 +87,18 @@ prettyConstraint bindEnv c =
             ]
       mergedEnv = mergeDuplicatedBindings env
       undoANFEnv = undoANFAndVV mergedEnv
-      boolSimplEnv = HashMap.map snd $ simplifyBooleanRefts undoANFEnv
+      boolSimplEnvDiff = simplifyBooleanRefts undoANFEnv
+      boolSimplEnv = HashMap.map snd $ HashMap.union boolSimplEnvDiff undoANFEnv
 
       simplifiedLhs = simplify $ inlineInSortedReft (`HashMap.lookup` boolSimplEnv) (slhs c)
       simplifiedRhs = simplify $ inlineInSortedReft (`HashMap.lookup` boolSimplEnv) (srhs c)
 
       prunedEnv =
-        dropLikelyIrrelevantBindings
-          (constraintSymbols simplifiedLhs simplifiedRhs)
+        if expr simplifiedRhs /= PFalse then
+          dropLikelyIrrelevantBindings
+            (constraintSymbols simplifiedLhs simplifiedRhs)
+            boolSimplEnv
+        else
           boolSimplEnv
       (renamedEnv, c') =
         shortenVarNames prunedEnv c { slhs = simplifiedLhs, srhs = simplifiedRhs }