Skip to content
Browse files

All the foreign calls remain IO

  • Loading branch information...
1 parent d25d870 commit 31a7a0e2f42bf88e89ddd87a4bcf36004da579c2 José Iborra committed Dec 28, 2009
Showing with 13 additions and 13 deletions.
  1. +8 −8 Bindings/Yices.hs
  2. +5 −5 Bindings/Yices/Internal.hsc
View
16 Bindings/Yices.hs
@@ -106,22 +106,22 @@ getVarFromDecl = c_mk_var_from_decl
getVar :: Context -> String -> IO (Maybe Expr)
getVar ctx name = getVarDecl ctx name >>= T.sequence . liftM (getVarFromDecl ctx)
-class YEval a where getValue :: Model -> VarDecl -> YDef a
+class YEval a where getValue :: Model -> VarDecl -> IO (YDef a)
instance YEval Bool where getValue = getBoolValue
instance YEval Int where getValue = getNatValue
-getBoolValue :: Model -> VarDecl -> YBool
-getBoolValue m vd = eatYBool $ c_get_value m vd
+getBoolValue :: Model -> VarDecl -> IO YBool
+getBoolValue m = liftM eatYBool . c_get_value m
-getNatValue :: Model -> VarDecl -> YDef Int
-getNatValue m vd = unsafePerformIO $ alloca $ \ptr -> do
+getNatValue :: Model -> VarDecl -> IO (YDef Int)
+getNatValue m vd = alloca $ \ptr -> do
code <- c_get_int_value m vd ptr
case code of
0 -> return YUndef
1 -> YDef . fromIntegral <$> peek ptr
-evaluateInModel :: Model -> Expr -> YBool
-evaluateInModel m = eatYBool . c_evaluate_in_model m
+evaluateInModel :: Model -> Expr -> IO YBool
+evaluateInModel m = liftM eatYBool . c_evaluate_in_model m
withVarIterator :: Context -> (VarIterator -> IO a) -> IO a
withVarIterator ctx f = do
@@ -210,7 +210,7 @@ getBoolModel ctx m = withVarIterator ctx $ \iter ->
then do
v <- c_iterator_next iter
name <- peekCString =<< c_get_var_decl_name v
- let value = getValue m v
+ value <- getValue m v
rest <- go
return ((name, value) : rest)
View
10 Bindings/Yices/Internal.hsc
@@ -143,7 +143,7 @@ foreign import ccall unsafe "yices_c.h yices_find_weighted_model"
--
foreign import ccall unsafe "yices_c.h yices_evaluate_in_model"
- c_evaluate_in_model :: Ptr YModel -> Ptr YExpr -> CInt
+ c_evaluate_in_model :: Ptr YModel -> Ptr YExpr -> IO CInt
--
@@ -173,7 +173,7 @@ foreign import ccall unsafe "yices_c.h yices_get_unsat_core"
--
foreign import ccall unsafe "yices_c.h yices_get_value"
- c_get_value :: Ptr YModel -> Ptr YVarDecl -> CInt
+ c_get_value :: Ptr YModel -> Ptr YVarDecl -> IO CInt
--
@@ -198,7 +198,7 @@ foreign import ccall unsafe "yices_c.h yices_get_bitvector_value"
--
foreign import ccall unsafe "yices_c.h yices_get_assertion_value"
- c_get_assertion_value :: Ptr YModel -> AssertionId -> CInt
+ c_get_assertion_value :: Ptr YModel -> AssertionId -> IO CInt
--
@@ -208,12 +208,12 @@ foreign import ccall unsafe "yices_c.h yices_display_model"
--
foreign import ccall unsafe "yices_c.h yices_get_cost"
- c_get_cost :: Ptr YModel -> CLLong
+ c_get_cost :: Ptr YModel -> IO CLLong
--
foreign import ccall unsafe "yices_c.h yices_get_cost_as_double"
- c_get_cost_as_double :: Ptr YModel -> CDouble
+ c_get_cost_as_double :: Ptr YModel -> IO CDouble
--

0 comments on commit 31a7a0e

Please sign in to comment.
Something went wrong with that request. Please try again.