From 799b36b8cbc5f76c4d9a72b8f6249f6f2a375321 Mon Sep 17 00:00:00 2001
From: Ryan Scott <rscott@galois.com>
Date: Wed, 4 Aug 2021 13:53:59 -0400
Subject: [PATCH] Bring SAW variables of type Bool into Cryptol expressions

Fixes #1404.
---
 CHANGES.md                 |  3 +++
 intTests/test1404/test.saw |  2 ++
 intTests/test1404/test.sh  |  3 +++
 src/SAWScript/Value.hs     | 11 ++++++++++-
 4 files changed, 18 insertions(+), 1 deletion(-)
 create mode 100644 intTests/test1404/test.saw
 create mode 100644 intTests/test1404/test.sh

diff --git a/CHANGES.md b/CHANGES.md
index e2dbcbe4db..99380cb3f7 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -24,6 +24,9 @@ A new `enable_lax_pointer_ordering` function exists, which relaxes the
 restrictions that Crucible imposes on comparisons between pointers from
 different allocation blocks.
 
+A SAW value of type `Bool` can now be brought into scope in Cryptol expressions
+as a value of type `Bit`.
+
 ## Changes
 
 * The linked-in version of ABC (based on the Haskell `abcBridge`
diff --git a/intTests/test1404/test.saw b/intTests/test1404/test.saw
new file mode 100644
index 0000000000..f290eaa69e
--- /dev/null
+++ b/intTests/test1404/test.saw
@@ -0,0 +1,2 @@
+let b = true;
+print {{ b }};
diff --git a/intTests/test1404/test.sh b/intTests/test1404/test.sh
new file mode 100644
index 0000000000..2315cc233c
--- /dev/null
+++ b/intTests/test1404/test.sh
@@ -0,0 +1,3 @@
+set -e
+
+$SAW test.saw
diff --git a/src/SAWScript/Value.hs b/src/SAWScript/Value.hs
index c884483ed2..7748fc78a5 100644
--- a/src/SAWScript/Value.hs
+++ b/src/SAWScript/Value.hs
@@ -574,6 +574,9 @@ extendEnv sc x mt md v rw =
          VString s ->
            do tt <- typedTermOfString sc (unpack s)
               pure $ CEnv.bindTypedTerm (ident, tt) ce
+         VBool b ->
+           do tt <- typedTermOfBool sc b
+              pure $ CEnv.bindTypedTerm (ident, tt) ce
          _ ->
            pure ce
      pure $
@@ -590,7 +593,7 @@ extendEnv sc x mt md v rw =
 
 typedTermOfString :: SharedContext -> String -> IO TypedTerm
 typedTermOfString sc str =
-  do let schema = Cryptol.Forall [] [] (Cryptol.tString (length str))
+  do let schema = Cryptol.tMono (Cryptol.tString (length str))
      bvNat <- scGlobalDef sc "Prelude.bvNat"
      bvNat8 <- scApply sc bvNat =<< scNat sc 8
      byteT <- scBitvector sc 8
@@ -599,6 +602,12 @@ typedTermOfString sc str =
      trm <- scVector sc byteT ts
      pure (TypedTerm (TypedTermSchema schema) trm)
 
+typedTermOfBool :: SharedContext -> Bool -> IO TypedTerm
+typedTermOfBool sc b =
+  do let schema = Cryptol.tMono Cryptol.tBit
+     trm <- scBool sc b
+     pure (TypedTerm (TypedTermSchema schema) trm)
+
 
 -- Other SAWScript Monads ------------------------------------------------------