Merge pull request #152 from GaloisInc/issue151

Adapt Conversion library to use `scGlobalDef` when building terms.
GaloisInc · Jan 25, 2021 · 0d1051d · 0d1051d
2 parents f6ebafd + 85252a8
commit 0d1051d
Show file tree

Hide file tree

Showing 3 changed files with 14 additions and 11 deletions.
diff --git 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
@@ -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
@@ -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 =