Generalize Queriable defaults and simplify

LeventErkok · Nov 6, 2024 · 58ccc2b · 58ccc2b
1 parent 8cc319a
commit 58ccc2b
Show file tree

Hide file tree

Showing 3 changed files with 8 additions and 19 deletions.
diff --git a/Data/SBV.hs b/Data/SBV.hs
@@ -1777,10 +1777,10 @@ class Queriable m a where
   embed   :: QueryResult a -> QueryT m a
 
   default project :: (a ~ t (SBV e), QueryResult a ~ t e, Traversable t, MonadIO m, SymVal e) => a -> QueryT m (QueryResult a)
-  project = mapM getValue
+  project = mapM project
 
   default embed :: (a ~ t (SBV e), QueryResult a ~ t e, Traversable t, MonadIO m, SymVal e) => QueryResult a -> QueryT m a
-  embed = pure . fmap literal
+  embed = mapM embed
   {-# MINIMAL create #-}
 
 -- | Generic 'Queriable' instance for 'SymVal' values

diff --git a/Documentation/SBV/Examples/Puzzles/DieHard.hs b/Documentation/SBV/Examples/Puzzles/DieHard.hs
@@ -54,20 +54,9 @@ type CState = State Integer Action
 instance Queriable IO SState where
   type QueryResult SState = CState
 
-  create = State <$> freshVar_ <*> freshVar_ <*> freshVar_
-
-  project State{big, small, action} = do b <- getValue big
-                                         s <- getValue small
-                                         a <- getValue action
-                                         pure State{ big    = b
-                                                   , small  = s
-                                                   , action = a
-                                                   }
-
-  embed State{big, small, action} = pure State{ big    = literal big
-                                              , small  = literal small
-                                              , action = literal action
-                                              }
+  create                = State <$> freshVar_ <*> freshVar_ <*> freshVar_
+  project (State b s a) = State <$> project b <*> project s <*> project a
+  embed   (State b s a) = State <$> embed   b <*> embed   s <*> embed   a
 
 -- | Solve the problem using a BMC search. We have:
 --

diff --git a/Documentation/SBV/Examples/WeakestPreconditions/Length.hs b/Documentation/SBV/Examples/WeakestPreconditions/Length.hs
@@ -47,9 +47,9 @@ instance (SymVal a, Show (f a), Show b) => Show (LenS (f a) b) where
 instance Queriable IO (LenS (SList Integer) SInteger) where
   type QueryResult (LenS (SList Integer) SInteger) = LenS [Integer] Integer
 
-  create                  = LenS <$> freshVar_   <*> freshVar_   <*> freshVar_
-  project LenS{xs, ys, l} = getValue xs >>= \vxs -> getValue ys >>= \vys -> getValue l >>= \vl -> pure LenS{xs = vxs, ys = vys, l = vl}
-  embed   LenS{xs, ys, l} = pure LenS{xs = literal xs, ys = literal ys, l = literal l}
+  create                 = LenS <$> freshVar_  <*> freshVar_  <*> freshVar_
+  project (LenS xs ys l) = LenS <$> project xs <*> project ys <*> project l
+  embed   (LenS xs ys l) = LenS <$> embed   xs <*> embed   ys <*> embed   l
 
 -- | Helper type synonym
 type S = LenS (SList Integer) SInteger