Skip to content

Commit

Permalink
Adapt Conversion library to use scGlobalDef when building terms.
Browse files Browse the repository at this point in the history
This corrects an oversight from PR #118, which changed the term
representation for defined constants in saw-core.

Fixes #151.
  • Loading branch information
Brian Huffman committed Jan 25, 2021
1 parent 17a26a2 commit 85252a8
Show file tree
Hide file tree
Showing 3 changed files with 14 additions and 11 deletions.
17 changes: 10 additions & 7 deletions saw-core/src/Verifier/SAW/Conversion.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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`
Expand Down
6 changes: 3 additions & 3 deletions saw-core/src/Verifier/SAW/Rewriter.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down
2 changes: 1 addition & 1 deletion saw-core/tests/src/Tests/Rewriter.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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 =
Expand Down

0 comments on commit 85252a8

Please sign in to comment.