From a7a158bf75b9730448b1ca82c8432c19de728782 Mon Sep 17 00:00:00 2001
From: Ryan Scott <ryan.gl.scott@gmail.com>
Date: Sat, 8 Oct 2022 08:58:05 -0400
Subject: [PATCH] Adapt to CLC#85
Fixes #57.
---
patches/parameterized-utils-2.1.5.0.patch | 15 +++++++
patches/sbv-9.0.patch | 48 +++++++++++++++++++++++
patches/singletons-base-3.1.patch | 17 ++++++++
patches/typelits-printf-0.2.0.0.patch | 41 +++++++++++++++++++
patches/winery-1.4.patch | 13 ++++++
5 files changed, 134 insertions(+)
create mode 100644 patches/sbv-9.0.patch
create mode 100644 patches/singletons-base-3.1.patch
create mode 100644 patches/typelits-printf-0.2.0.0.patch
create mode 100644 patches/winery-1.4.patch
diff --git a/patches/parameterized-utils-2.1.5.0.patch b/patches/parameterized-utils-2.1.5.0.patch
index bc248c43..7273b46a 100644
--- a/patches/parameterized-utils-2.1.5.0.patch
+++ b/patches/parameterized-utils-2.1.5.0.patch
@@ -72,6 +72,21 @@ index 6118c9d..fcfbfdc 100644
{-|
Copyright : (c) Galois, Inc 2021
+diff --git a/src/Data/Parameterized/NatRepr.hs b/src/Data/Parameterized/NatRepr.hs
+index 64465f9..e71d0a2 100644
+--- a/src/Data/Parameterized/NatRepr.hs
++++ b/src/Data/Parameterized/NatRepr.hs
+@@ -134,7 +134,9 @@ import Data.Data
+ import Data.Type.Equality as Equality
+ import Data.Void as Void
+ import Numeric.Natural
+-import GHC.TypeNats as TypeNats
++import GHC.TypeNats ( KnownNat, Nat, SomeNat(..)
++ , type (+), type (-), type (*), type (<=)
++ , someNatVal )
+ import Unsafe.Coerce
+
+ import Data.Parameterized.Axiom
diff --git a/src/Data/Parameterized/Some.hs b/src/Data/Parameterized/Some.hs
index 3df9359..75e9c55 100644
--- a/src/Data/Parameterized/Some.hs
diff --git a/patches/sbv-9.0.patch b/patches/sbv-9.0.patch
new file mode 100644
index 00000000..b1e64bef
--- /dev/null
+++ b/patches/sbv-9.0.patch
@@ -0,0 +1,48 @@
+diff --git a/Data/SBV.hs b/Data/SBV.hs
+index 907913d..69cdae9 100644
+--- a/Data/SBV.hs
++++ b/Data/SBV.hs
+@@ -464,7 +464,7 @@ import Data.SBV.Control.Types (SMTReasonUnknown(..), Logic(..))
+ import qualified Data.SBV.Utils.CrackNum as CN
+
+ import Data.Proxy (Proxy(..))
+-import GHC.TypeLits
++import GHC.TypeLits (KnownNat, type (+), type (-), type (<=))
+
+ import Prelude hiding((+), (-), (*)) -- to avoid the haddock ambiguity
+
+@@ -939,7 +939,7 @@ the 'Data.SBV.Core.Model.Uninterpreted' class.
+ -}
+
+ {- $enumerations
+-If the uninterpreted sort definition takes the form of an enumeration (i.e., a simple data type with all nullary constructors), then
++If the uninterpreted sort definition takes the form of an enumeration (i.e., a simple data type with all nullary constructors), then
+ tou can use the 'mkSymbolicEnumeration' functio to turn it into an enumeration in SMTLib.
+ A simple example is:
+
+diff --git a/Data/SBV/Client/BaseIO.hs b/Data/SBV/Client/BaseIO.hs
+index 512cee7..6a21f2a 100644
+--- a/Data/SBV/Client/BaseIO.hs
++++ b/Data/SBV/Client/BaseIO.hs
+@@ -39,7 +39,7 @@ import Data.SBV.Provers.Prover (Provable, SExecutable, ThmResult)
+ import Data.SBV.SMT.SMT (AllSatResult, SafeResult, SatResult,
+ OptimizeResult)
+
+-import GHC.TypeLits
++import GHC.TypeLits (ErrorMessage(..), KnownNat, TypeError)
+ import Data.Kind
+
+ import Data.Int
+diff --git a/Data/SBV/Core/Data.hs b/Data/SBV/Core/Data.hs
+index c600e6a..cd5a64a 100644
+--- a/Data/SBV/Core/Data.hs
++++ b/Data/SBV/Core/Data.hs
+@@ -62,7 +62,7 @@ module Data.SBV.Core.Data
+ , QueryState(..), QueryT(..), SMTProblem(..)
+ ) where
+
+-import GHC.TypeLits
++import GHC.TypeLits (Nat)
+
+ import GHC.Generics (Generic)
+ import GHC.Exts (IsList(..))
diff --git a/patches/singletons-base-3.1.patch b/patches/singletons-base-3.1.patch
new file mode 100644
index 00000000..9996b3bc
--- /dev/null
+++ b/patches/singletons-base-3.1.patch
@@ -0,0 +1,17 @@
+diff --git a/src/GHC/TypeLits/Singletons/Internal.hs b/src/GHC/TypeLits/Singletons/Internal.hs
+index 87c4b14..9a7b94c 100644
+--- a/src/GHC/TypeLits/Singletons/Internal.hs
++++ b/src/GHC/TypeLits/Singletons/Internal.hs
+@@ -49,7 +49,11 @@ import Data.Singletons.Decide
+ import Data.Singletons.TH
+ import GHC.Show (appPrec, appPrec1)
+ import GHC.Stack (HasCallStack)
+-import GHC.TypeLits as TL
++import qualified GHC.TypeLits as TL
++import GHC.TypeLits ( KnownChar, KnownNat, KnownSymbol, Natural
++ , SomeChar(..), SomeNat(..), SomeSymbol(..), Symbol
++ , type (^), type (<=?), charVal, sameChar, sameNat
++ , sameSymbol, someCharVal, someSymbolVal, symbolVal )
+ import qualified GHC.TypeNats as TN
+ import Unsafe.Coerce
+
diff --git a/patches/typelits-printf-0.2.0.0.patch b/patches/typelits-printf-0.2.0.0.patch
new file mode 100644
index 00000000..e814c389
--- /dev/null
+++ b/patches/typelits-printf-0.2.0.0.patch
@@ -0,0 +1,41 @@
+diff --git a/src/GHC/TypeLits/Printf/Internal.hs b/src/GHC/TypeLits/Printf/Internal.hs
+index 6cd55f9..88449c2 100644
+--- a/src/GHC/TypeLits/Printf/Internal.hs
++++ b/src/GHC/TypeLits/Printf/Internal.hs
+@@ -62,7 +62,8 @@ import Data.Proxy
+ import Data.Symbol.Utils
+ import Data.Word
+ import GHC.OverloadedLabels
+-import GHC.TypeLits
++import GHC.TypeLits ( ErrorMessage(..), KnownSymbol, Symbol
++ , TypeError, symbolVal )
+ import GHC.TypeLits.Printf.Parse
+ import Numeric.Natural
+ import qualified Data.Text as T
+diff --git a/src/GHC/TypeLits/Printf/Internal/Parser.hs b/src/GHC/TypeLits/Printf/Internal/Parser.hs
+index cf8c6df..fe51a1f 100644
+--- a/src/GHC/TypeLits/Printf/Internal/Parser.hs
++++ b/src/GHC/TypeLits/Printf/Internal/Parser.hs
+@@ -11,7 +11,8 @@ module GHC.TypeLits.Printf.Internal.Parser where
+ import Data.Kind
+ import Data.Type.Bool
+ import Data.Type.Equality
+-import GHC.TypeLits
++import GHC.TypeLits ( AppendSymbol, ErrorMessage(..), Nat, Symbol
++ , TypeError, type (+), type (*) )
+
+ -- | A type synonym for a single-character symbol. Ideally this would just
+ -- be 'Char', but we don't have chars at the type level. So, if you see
+diff --git a/src/GHC/TypeLits/Printf/Parse.hs b/src/GHC/TypeLits/Printf/Parse.hs
+index 263ffcb..513e523 100644
+--- a/src/GHC/TypeLits/Printf/Parse.hs
++++ b/src/GHC/TypeLits/Printf/Parse.hs
+@@ -30,7 +30,7 @@ module GHC.TypeLits.Printf.Parse (
+
+ import Data.Proxy
+ import Data.Text (Text)
+-import GHC.TypeLits hiding (natVal)
++import GHC.TypeLits (AppendSymbol, KnownSymbol, Symbol, symbolVal)
+ import GHC.TypeLits.Printf.Internal.Parser
+ import GHC.TypeNats
+ import Numeric.Natural
diff --git a/patches/winery-1.4.patch b/patches/winery-1.4.patch
new file mode 100644
index 00000000..6f7581fc
--- /dev/null
+++ b/patches/winery-1.4.patch
@@ -0,0 +1,13 @@
+diff --git a/src/Codec/Winery/Class.hs b/src/Codec/Winery/Class.hs
+index d9a5f65..da96f1b 100644
+--- a/src/Codec/Winery/Class.hs
++++ b/src/Codec/Winery/Class.hs
+@@ -116,7 +116,7 @@ import Unsafe.Coerce
+ import GHC.Float (castWord32ToFloat, castWord64ToDouble)
+ import GHC.Natural
+ import GHC.Generics
+-import GHC.TypeLits
++import GHC.TypeLits (KnownSymbol, symbolVal)
+
+ -- | Serialisable datatype
+ --
--
GitLab