Merge pull request #667 from ucsd-progsys/fd/changelog-and-cleanups

Update changelog and introduce some CPP to handle both ghc 9.6 and 9.4
ucsd-progsys · Dec 5, 2023 · d5b8b13 · d5b8b13
2 parents bc8fa31 + 2983cf9
commit d5b8b13
Show file tree

Hide file tree

Showing 3 changed files with 22 additions and 2 deletions.
diff --git a/CHANGES.md b/CHANGES.md
@@ -2,6 +2,19 @@
 
 ## NEXT
 
+## 0.9.2.5
+
+- Simplified the equalities dumped by PLE [#569](https://github.com/ucsd-progsys/liquid-fixpoint/issues/569) [#605](https://github.com/ucsd-progsys/liquid-fixpoint/issues/605)
+- Adopt smtlib-backends for interactions with the SMT solvers [#641](https://github.com/ucsd-progsys/liquid-fixpoint/issues/641)
+
+## 0.8.10.2
+
+- Dump equalities discovered by PLE [#491](https://github.com/ucsd-progsys/liquid-fixpoint/pull/491) [#569](https://github.com/ucsd-progsys/liquid-fixpoint/issues/569)
+- Dump prettified version of constraints [#473](https://github.com/ucsd-progsys/liquid-fixpoint/pull/473)
+- Constraints now indicate the source code location that originated them [#471](https://github.com/ucsd-progsys/liquid-fixpoint/pull/471)
+
+## 0.8.6.4
+
 - Fix bugs in PLE
 - Move to GHC 8.6.4 
 - Add `fuel` parameter to debug unfolding in PLE

diff --git a/liquid-fixpoint.cabal b/liquid-fixpoint.cabal
@@ -25,7 +25,7 @@ copyright:          2010-17 Ranjit Jhala, University of California, San Diego.
 license:            BSD-3-Clause
 license-file:       LICENSE
 build-type:         Simple
-tested-with:        GHC == 7.10.3, GHC == 8.0.1, GHC == 8.4.3, GHC == 8.6.4, GHC == 8.10.1, GHC == 8.10.7
+tested-with:        GHC == 9.6.3, GHC == 9.4.7, GHC == 9.2.3
 extra-source-files: tests/neg/*.fq
                     tests/pos/*.fq
                     unix/Language/Fixpoint/Utils/*.hs

diff --git a/src/Language/Fixpoint/Solver/Extensionality.hs b/src/Language/Fixpoint/Solver/Extensionality.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE CPP                  #-}
 {-# LANGUAGE FlexibleInstances    #-}
 {-# LANGUAGE PatternGuards        #-}
 {-# LANGUAGE FlexibleContexts     #-}
@@ -201,11 +202,17 @@ initST env dd = ExSt 0 (d:dd) env mempty mempty mempty
   where
     -- NV: hardcore Haskell pairs because they do not appear in DataDecl (why?)
     d = mytracepp "Tuple DataDecl" $ DDecl (symbolFTycon (dummyLoc tupConName)) 2 [ct]
+#if MIN_TOOL_VERSION_ghc(9,6,0)
     ct = DCtor (dummyLoc (symbol "GHC.Tuple.Prim.(,)")) [
             DField (dummyLoc (symbol "lqdc$select$GHC.Tuple.Prim.(,)$1")) (FVar 0)
           , DField (dummyLoc (symbol "lqdc$select$GHC.Tuple.Prim.(,)$2")) (FVar 1)
           ]
-
+#else
+    ct = DCtor (dummyLoc (symbol "GHC.Tuple.(,)")) [
+            DField (dummyLoc (symbol "lqdc$select$GHC.Tuple.(,)$1")) (FVar 0)
+          , DField (dummyLoc (symbol "lqdc$select$GHC.Tuple.(,)$2")) (FVar 1)
+          ]
+#endif
 
 setBEnv :: BindEnv a -> Ex a ()
 setBEnv benv = modify (\st -> st{exbenv = benv})