From 85252a867b2dbc77a79ca4d829f44326f810b975 Mon Sep 17 00:00:00 2001
From: Brian Huffman <huffman@galois.com>
Date: Mon, 25 Jan 2021 10:07:22 -0800
Subject: [PATCH] Adapt Conversion library to use `scGlobalDef` when building
 terms.

This corrects an oversight from PR #118, which changed the term
representation for defined constants in saw-core.

Fixes #151.
---
 saw-core/src/Verifier/SAW/Conversion.hs | 17 ++++++++++-------
 saw-core/src/Verifier/SAW/Rewriter.hs   |  6 +++---
 saw-core/tests/src/Tests/Rewriter.hs    |  2 +-
 3 files changed, 14 insertions(+), 11 deletions(-)

diff --git a/saw-core/src/Verifier/SAW/Conversion.hs b/saw-core/src/Verifier/SAW/Conversion.hs
index d85dcfabe3..8fbd8d74e4 100644
--- a/saw-core/src/Verifier/SAW/Conversion.hs
+++ b/saw-core/src/Verifier/SAW/Conversion.hs
@@ -352,13 +352,16 @@ instance Matchable (Prim.Vec Term Term) where
 -- Term builders
 
 newtype TermBuilder v =
-    TermBuilder { runTermBuilder :: forall m. Monad m => (TermF Term -> m Term) -> m v }
+  TermBuilder
+  { runTermBuilder ::
+      forall m. Monad m => (Ident -> m Term) -> (TermF Term -> m Term) -> m v
+  }
 
 instance Monad TermBuilder where
-  m >>= h = TermBuilder $ \mk -> do
-    r <- runTermBuilder m mk
-    runTermBuilder (h r) mk
-  return v = TermBuilder $ \_ -> return v
+  m >>= h = TermBuilder $ \mg mk -> do
+    r <- runTermBuilder m mg mk
+    runTermBuilder (h r) mg mk
+  return v = TermBuilder $ \_ _ -> return v
 
 instance Functor TermBuilder where
     fmap = liftM
@@ -368,10 +371,10 @@ instance Applicative TermBuilder where
     (<*>) = ap
 
 mkTermF :: TermF Term -> TermBuilder Term
-mkTermF tf = TermBuilder (\mk -> mk tf)
+mkTermF tf = TermBuilder (\_ mk -> mk tf)
 
 mkGlobalDef :: Ident -> TermBuilder Term
-mkGlobalDef i = mkTermF (FTermF (GlobalDef i))
+mkGlobalDef i = TermBuilder (\mg _ -> mg i)
 
 infixl 9 `mkApp`
 infixl 9 `pureApp`
diff --git a/saw-core/src/Verifier/SAW/Rewriter.hs b/saw-core/src/Verifier/SAW/Rewriter.hs
index 981d483ae1..acc75e49d3 100644
--- a/saw-core/src/Verifier/SAW/Rewriter.hs
+++ b/saw-core/src/Verifier/SAW/Rewriter.hs
@@ -572,7 +572,7 @@ rewriteSharedTerm sc ss t0 =
            -- print (Net.toPat conv)
            case runConversion conv t of
              Nothing -> apply rules t
-             Just tb -> rewriteAll =<< runTermBuilder tb (scTermF sc)
+             Just tb -> rewriteAll =<< runTermBuilder tb (scGlobalDef sc) (scTermF sc)
 
 -- | Type-safe rewriter for shared terms
 rewriteSharedTermTypeSafe
@@ -644,7 +644,7 @@ rewriteSharedTermTypeSafe sc ss t0 =
     apply (Right conv : rules) t =
       case runConversion conv t of
         Nothing -> apply rules t
-        Just tb -> rewriteAll =<< runTermBuilder tb (scTermF sc)
+        Just tb -> rewriteAll =<< runTermBuilder tb (scGlobalDef sc) (scTermF sc)
 
 -- | Generate a new SharedContext that normalizes terms as it builds them.
 rewritingSharedContext :: SharedContext -> Simpset -> SharedContext
@@ -677,7 +677,7 @@ rewritingSharedContext sc ss = sc'
     apply (Right conv : rules) t =
       case runConversion conv t of
         Nothing -> apply rules t
-        Just tb -> runTermBuilder tb (scTermF sc')
+        Just tb -> runTermBuilder tb (scGlobalDef sc) (scTermF sc')
 
 
 -- FIXME: is there some way to have sensable term replacement in the presence of loose variables
diff --git a/saw-core/tests/src/Tests/Rewriter.hs b/saw-core/tests/src/Tests/Rewriter.hs
index 4af625887b..66854f7539 100644
--- a/saw-core/tests/src/Tests/Rewriter.hs
+++ b/saw-core/tests/src/Tests/Rewriter.hs
@@ -22,7 +22,7 @@ import Test.Tasty
 import Test.Tasty.HUnit
 
 scMkTerm :: SharedContext -> TermBuilder Term -> IO Term
-scMkTerm sc t = runTermBuilder t (scTermF sc)
+scMkTerm sc t = runTermBuilder t (scGlobalDef sc) (scTermF sc)
 
 rewriter_tests :: [TestTree]
 rewriter_tests =