From 24d53a963c2a2d11a118cfaa98956a69f5c8c6d5 Mon Sep 17 00:00:00 2001
From: Ryan Scott <rscott@galois.com>
Date: Fri, 10 Mar 2023 14:13:50 -0500
Subject: [PATCH] Adapt to changes in GaloisInc/what4#226

GaloisInc/what4#226 adds some additional methods to `SMTWriter` that
`language-sally` must implement.
---
 dependencies/what4           | 2 +-
 language-sally.cabal         | 2 +-
 src/Language/Sally/Writer.hs | 5 +++++
 3 files changed, 7 insertions(+), 2 deletions(-)

diff --git a/dependencies/what4 b/dependencies/what4
index 6f5e0fe..6c462cd 160000
--- a/dependencies/what4
+++ b/dependencies/what4
@@ -1 +1 @@
-Subproject commit 6f5e0fe9bef58234603ccf6914c32ea1ba2f9766
+Subproject commit 6c462cd46e0ea9ebbfbd6b6ea237984eeb3dc72a
diff --git a/language-sally.cabal b/language-sally.cabal
index e394d3a..e27cb6f 100644
--- a/language-sally.cabal
+++ b/language-sally.cabal
@@ -27,7 +27,7 @@ common dependencies
   build-depends:
     , base                     >=4.8   && <4.17
     , parameterized-utils      >=2.0   && <2.2
-    , what4                    >=1.3
+    , what4                    >=1.4
     , what4-transition-system  >=0.0.3
 
 library
diff --git a/src/Language/Sally/Writer.hs b/src/Language/Sally/Writer.hs
index 4d799ad..2fb8075 100644
--- a/src/Language/Sally/Writer.hs
+++ b/src/Language/Sally/Writer.hs
@@ -257,6 +257,11 @@ instance SMTLib2Tweaks a => SMTWriter (SallyWriter a) where
     let resolveArg (var, Some tp) = (var, asSMT2Type @a tp)
      in SMT2.defineFun f (resolveArg <$> args) (asSMT2Type @a return_type) <$> e
 
+  synthFunCommand _proxy f args ret_tp =
+    pure $ SMT2.synthFun f (map (\(var, Some tp) -> (var, asSMT2Type @a tp)) args) (asSMT2Type @a ret_tp)
+  declareVarCommand _proxy v tp = pure $ SMT2.declareVar v (asSMT2Type @a tp)
+  constraintCommand _proxy e = SMT2.constraint <$> e
+
   stringTerm bs = pure $ smtlib2StringTerm @a bs
   stringLength x = smtlib2StringLength @a <$> x
   stringAppend xs = smtlib2StringAppend @a <$> sequence xs