1. Iago Abal
  2. z3-haskell

Commits

Iago Abal  committed d18cf1d

Remove most of the marshalling boilerplate in Z3.Base

  • Participants
  • Parent commits d74bfb0
  • Branches default

Comments (0)

Files changed (1)

File Z3/Base.hs

View file
 {-# LANGUAGE GeneralizedNewtypeDeriving #-}
 {-# LANGUAGE PatternGuards              #-}
 {-# LANGUAGE TupleSections              #-}
+{-# LANGUAGE TypeFamilies               #-}
 
 -- |
 -- Module    : Z3.Base
 import Data.Word
 import Foreign hiding ( toBool, newForeignPtr )
 import Foreign.C
-  ( CInt, CUInt, CLLong, CULLong
+  ( CDouble, CInt, CUInt, CLLong, CULLong, CString
   , peekCString
   , withCString )
 import Foreign.Concurrent
 --
 -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga165e38ddfc928f586cb738cdf6c5f216>
 contextToString :: Context -> IO String
-contextToString c =
-  checkError c $ z3_context_to_string (unContext c) >>= peekCString
+contextToString = liftFun0 z3_context_to_string
 
 -- | Alias for 'contextToString'.
 showContext :: Context -> IO String
 mkIntSymbol :: Integral int => Context -> int -> IO Symbol
 mkIntSymbol ctx i
   | 0 <= i && i <= 2^(30::Int)-1
-  = Symbol <$> z3_mk_int_symbol (unContext ctx) (fromIntegral i)
+  = liftVal ctx =<< z3_mk_int_symbol (unContext ctx) (fromIntegral i)
   | otherwise
   = error "Z3.Base.mkIntSymbol: invalid range"
 
 --
 -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gafebb0d3c212927cf7834c3a20a84ecae>
 mkStringSymbol :: Context -> String -> IO Symbol
-mkStringSymbol ctx s =
-  withCString s $ \cs ->
-    checkError ctx $
-      Symbol <$> z3_mk_string_symbol (unContext ctx) cs
+mkStringSymbol = liftFun1 z3_mk_string_symbol
 
 ---------------------------------------------------------------------
 -- Sorts
 --
 -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga736e88741af1c178cbebf94c49aa42de>
 mkUninterpretedSort :: Context -> Symbol -> IO Sort
-mkUninterpretedSort c sy = checkError c $
-  Sort <$> z3_mk_uninterpreted_sort (unContext c) (unSymbol sy)
+mkUninterpretedSort = liftFun1 z3_mk_uninterpreted_sort
 
 -- | Create the /Boolean/ type.
 --
 -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gacdc73510b69a010b71793d429015f342>
 mkBoolSort :: Context -> IO Sort
-mkBoolSort c = checkError c $ Sort <$> z3_mk_bool_sort (unContext c)
+mkBoolSort = liftFun0 z3_mk_bool_sort
 
 -- | Create an /integer/ type.
 --
 -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga6cd426ab5748653b77d389fd3eac1015>
 mkIntSort :: Context -> IO Sort
-mkIntSort c = checkError c $ Sort <$> z3_mk_int_sort (unContext c)
+mkIntSort = liftFun0 z3_mk_int_sort
 
 -- | Create a /real/ type.
 --
 -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga40ef93b9738485caed6dc84631c3c1a0>
 mkRealSort :: Context -> IO Sort
-mkRealSort c = checkError c $ Sort <$> z3_mk_real_sort (unContext c)
+mkRealSort = liftFun0 z3_mk_real_sort
 
 -- | Create a bit-vector type of the given size.
 --
 --
 -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaeed000a1bbb84b6ca6fdaac6cf0c1688>
 mkBvSort :: Context -> Int -> IO Sort
-mkBvSort c n = checkError c $ Sort <$> z3_mk_bv_sort (unContext c) (fromIntegral n)
+mkBvSort = liftFun1 z3_mk_bv_sort
 
 -- | Create an array type
 --
 -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gafe617994cce1b516f46128e448c84445>
 --
 mkArraySort :: Context -> Sort -> Sort -> IO Sort
-mkArraySort c dom rng = checkError c $ Sort <$> z3_mk_array_sort (unContext c) (unSort dom) (unSort rng)
+mkArraySort = liftFun2 z3_mk_array_sort
 
 -- | Create a tuple type
 --
 mkFuncDecl ctx smb dom rng =
   withArray (map unSort dom) $ \c_dom ->
     checkError ctx $
-      FuncDecl <$> z3_mk_func_decl (unContext ctx)
-                                   (unSymbol smb)
-                                   (genericLength dom)
-                                   c_dom
-                                   (unSort rng)
+      liftVal ctx =<< z3_mk_func_decl (unContext ctx)
+                                      (unSymbol smb)
+                                      (genericLength dom)
+                                      c_dom
+                                      (unSort rng)
 
 -- | Create a constant or function application.
 --
 -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga33a202d86bf628bfab9b6f437536cebe>
 mkApp :: Context -> FuncDecl -> [AST] -> IO AST
 mkApp ctx fd args =
-  withArray (map unAST args) $ \pargs ->
+  withAstArray args $ \numArgs pargs ->
     checkError ctx $
-      AST <$> z3_mk_app ctxPtr fdPtr numArgs pargs
+      liftVal ctx =<< z3_mk_app ctxPtr fdPtr numArgs pargs
   where ctxPtr  = unContext ctx
         fdPtr   = unFuncDecl fd
-        numArgs = genericLength args
 
 -- | Declare and create a constant.
 --
 -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga093c9703393f33ae282ec5e8729354ef>
 mkConst :: Context -> Symbol -> Sort -> IO AST
-mkConst c x s = checkError c $ AST <$> z3_mk_const (unContext c) (unSymbol x) (unSort s)
+mkConst = liftFun2 z3_mk_const
 
 -- TODO Constants and Applications: Z3_mk_fresh_func_decl
 -- TODO Constants and Applications: Z3_mk_fresh_const
 --
 -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gae898e7380409bbc57b56cc5205ef1db7>
 mkTrue :: Context -> IO AST
-mkTrue c = checkError c $ AST <$> z3_mk_true (unContext c)
+mkTrue = liftFun0 z3_mk_true
 
 -- | Create an AST node representing /false/.
 --
 -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga5952ac17671117a02001fed6575c778d>
 mkFalse :: Context -> IO AST
-mkFalse c = checkError c $ AST <$> z3_mk_false (unContext c)
+mkFalse = liftFun0 z3_mk_false
 
 -- | Create an AST node representing /l = r/.
 --
 -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga95a19ce675b70e22bb0401f7137af37c>
 mkEq :: Context -> AST -> AST -> IO AST
-mkEq = liftAst2 z3_mk_eq
+mkEq = liftFun2 z3_mk_eq
 
 -- | The distinct construct is used for declaring the arguments pairwise
 -- distinct.
 --
 -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga3329538091996eb7b3dc677760a61072>
 mkNot :: Context -> AST -> IO AST
-mkNot = liftAst1 z3_mk_not
+mkNot = liftFun1 z3_mk_not
 
 -- | Create an AST node representing an if-then-else: /ite(t1, t2, t3)/.
 --
 -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga94417eed5c36e1ad48bcfc8ad6e83547>
 mkIte :: Context -> AST -> AST -> AST -> IO AST
-mkIte c g e1 e2 =
-  checkError c $ AST <$> z3_mk_ite (unContext c) (unAST g) (unAST e1) (unAST e2)
+mkIte = liftFun3 z3_mk_ite
 
 -- | Create an AST node representing /t1 iff t2/.
 --
 -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga930a8e844d345fbebc498ac43a696042>
 mkIff :: Context -> AST -> AST -> IO AST
-mkIff = liftAst2 z3_mk_iff
+mkIff = liftFun2 z3_mk_iff
 
 -- | Create an AST node representing /t1 implies t2/.
 --
 -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gac829c0e25bbbd30343bf073f7b524517>
 mkImplies :: Context -> AST -> AST -> IO AST
-mkImplies = liftAst2 z3_mk_implies
+mkImplies = liftFun2 z3_mk_implies
 
 -- | Create an AST node representing /t1 xor t2/.
 --
 -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gacc6d1b848032dec0c4617b594d4229ec>
 mkXor :: Context -> AST -> AST -> IO AST
-mkXor = liftAst2 z3_mk_xor
+mkXor = liftFun2 z3_mk_xor
 
 -- | Create an AST node representing args[0] and ... and args[num_args-1].
 --
 --
 -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gadcd2929ad732937e25f34277ce4988ea>
 mkUnaryMinus :: Context -> AST -> IO AST
-mkUnaryMinus = liftAst1 z3_mk_unary_minus
+mkUnaryMinus = liftFun1 z3_mk_unary_minus
 
 -- | Create an AST node representing arg1 div arg2.
 --
 -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga1ac60ee8307af8d0b900375914194ff3>
 mkDiv :: Context -> AST -> AST -> IO AST
-mkDiv = liftAst2 z3_mk_div
+mkDiv = liftFun2 z3_mk_div
 
 -- | Create an AST node representing arg1 mod arg2.
 --
 -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga8e350ac77e6b8fe805f57efe196e7713>
 mkMod :: Context -> AST -> AST -> IO AST
-mkMod = liftAst2 z3_mk_mod
+mkMod = liftFun2 z3_mk_mod
 
 -- | Create an AST node representing arg1 rem arg2.
 --
 -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga2fcdb17f9039bbdaddf8a30d037bd9ff>
 mkRem :: Context -> AST -> AST -> IO AST
-mkRem = liftAst2 z3_mk_rem
+mkRem = liftFun2 z3_mk_rem
 
 -- | Create less than.
 --
 -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga58a3dc67c5de52cf599c346803ba1534>
 mkLt :: Context -> AST -> AST -> IO AST
-mkLt = liftAst2 z3_mk_lt
+mkLt = liftFun2 z3_mk_lt
 
 -- | Create less than or equal to.
 --
 -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaa9a33d11096841f4e8c407f1578bc0bf>
 mkLe :: Context -> AST -> AST -> IO AST
-mkLe = liftAst2 z3_mk_le
+mkLe = liftFun2 z3_mk_le
 
 -- | Create greater than.
 --
 -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga46167b86067586bb742c0557d7babfd3>
 mkGt :: Context -> AST -> AST -> IO AST
-mkGt = liftAst2 z3_mk_gt
+mkGt = liftFun2 z3_mk_gt
 
 -- | Create greater than or equal to.
 --
 -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gad9245cbadb80b192323d01a8360fb942>
 mkGe :: Context -> AST -> AST -> IO AST
-mkGe = liftAst2 z3_mk_ge
+mkGe = liftFun2 z3_mk_ge
 
 -- | Coerce an integer to a real.
 --
 -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga7130641e614c7ebafd28ae16a7681a21>
 mkInt2Real :: Context -> AST -> IO AST
-mkInt2Real = liftAst1 z3_mk_int2real
+mkInt2Real = liftFun1 z3_mk_int2real
 
 -- | Coerce a real to an integer.
 --
 -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga759b6563ba1204aae55289009a3fdc6d>
 mkReal2Int :: Context -> AST -> IO AST
-mkReal2Int = liftAst1 z3_mk_real2int
+mkReal2Int = liftFun1 z3_mk_real2int
 
 -- | Check if a real number is an integer.
 --
 -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaac2ad0fb04e4900fdb4add438d137ad3>
 mkIsInt :: Context -> AST -> IO AST
-mkIsInt = liftAst1 z3_mk_is_int
+mkIsInt = liftFun1 z3_mk_is_int
 
 ---------------------------------------------------------------------
 -- Bit-vectors
 --
 -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga36cf75c92c54c1ca633a230344f23080>
 mkBvnot :: Context -> AST -> IO AST
-mkBvnot = liftAst1 z3_mk_bvnot
+mkBvnot = liftFun1 z3_mk_bvnot
 
 -- | Take conjunction of bits in vector, return vector of length 1.
 --
 -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaccc04f2b58903279b1b3be589b00a7d8>
 mkBvredand :: Context -> AST -> IO AST
-mkBvredand = liftAst1 z3_mk_bvredand
+mkBvredand = liftFun1 z3_mk_bvredand
 
 -- | Take disjunction of bits in vector, return vector of length 1.
 --
 -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gafd18e127c0586abf47ad9cd96895f7d2>
 mkBvredor :: Context -> AST -> IO AST
-mkBvredor = liftAst1 z3_mk_bvredor
+mkBvredor = liftFun1 z3_mk_bvredor
 
 -- | Bitwise and.
 --
 -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gab96e0ea55334cbcd5a0e79323b57615d>
 mkBvand :: Context -> AST -> AST -> IO AST
-mkBvand = liftAst2 z3_mk_bvand
+mkBvand = liftFun2 z3_mk_bvand
 
 -- | Bitwise or.
 --
 -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga77a6ae233fb3371d187c6d559b2843f5>
 mkBvor :: Context -> AST -> AST -> IO AST
-mkBvor = liftAst2 z3_mk_bvor
+mkBvor = liftFun2 z3_mk_bvor
 
 -- | Bitwise exclusive-or.
 --
 -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga0a3821ea00b1c762205f73e4bc29e7d8>
 mkBvxor :: Context -> AST -> AST -> IO AST
-mkBvxor = liftAst2 z3_mk_bvxor
+mkBvxor = liftFun2 z3_mk_bvxor
 
 -- | Bitwise nand.
 --
 -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga96dc37d36efd658fff5b2b4df49b0e61>
 mkBvnand :: Context -> AST -> AST -> IO AST
-mkBvnand = liftAst2 z3_mk_bvnand
+mkBvnand = liftFun2 z3_mk_bvnand
 
 -- | Bitwise nor.
 --
 -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gabf15059e9e8a2eafe4929fdfd259aadb>
 mkBvnor :: Context -> AST -> AST -> IO AST
-mkBvnor = liftAst2 z3_mk_bvnor
+mkBvnor = liftFun2 z3_mk_bvnor
 
 -- | Bitwise xnor.
 --
 -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga784f5ca36a4b03b93c67242cc94b21d6>
 mkBvxnor :: Context -> AST -> AST -> IO AST
-mkBvxnor = liftAst2 z3_mk_bvxnor
+mkBvxnor = liftFun2 z3_mk_bvxnor
 
 -- | Standard two's complement unary minus.
 --
 -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga0c78be00c03eda4ed6a983224ed5c7b7
 mkBvneg :: Context -> AST -> IO AST
-mkBvneg = liftAst1 z3_mk_bvneg
+mkBvneg = liftFun1 z3_mk_bvneg
 
 -- | Standard two's complement addition.
 --
 -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga819814e33573f3f9948b32fdc5311158>
 mkBvadd :: Context -> AST -> AST -> IO AST
-mkBvadd = liftAst2 z3_mk_bvadd
+mkBvadd = liftFun2 z3_mk_bvadd
 
 -- | Standard two's complement subtraction.
 --
 -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga688c9aa1347888c7a51be4e46c19178e>
 mkBvsub :: Context -> AST -> AST -> IO AST
-mkBvsub = liftAst2 z3_mk_bvsub
+mkBvsub = liftFun2 z3_mk_bvsub
 
 -- | Standard two's complement multiplication.
 --
 -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga6abd3dde2a1ceff1704cf7221a72258c>
 mkBvmul :: Context -> AST -> AST -> IO AST
-mkBvmul = liftAst2 z3_mk_bvmul
+mkBvmul = liftFun2 z3_mk_bvmul
 
 -- | Unsigned division.
 --
 -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga56ce0cd61666c6f8cf5777286f590544>
 mkBvudiv :: Context -> AST -> AST -> IO AST
-mkBvudiv = liftAst2 z3_mk_bvudiv
+mkBvudiv = liftFun2 z3_mk_bvudiv
 
 -- | Two's complement signed division.
 --
 -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gad240fedb2fda1c1005b8e9d3c7f3d5a0>
 mkBvsdiv :: Context -> AST -> AST -> IO AST
-mkBvsdiv = liftAst2 z3_mk_bvsdiv
+mkBvsdiv = liftFun2 z3_mk_bvsdiv
 
 -- | Unsigned remainder.
 --
 -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga5df4298ec835e43ddc9e3e0bae690c8d>
 mkBvurem :: Context -> AST -> AST -> IO AST
-mkBvurem = liftAst2 z3_mk_bvurem
+mkBvurem = liftFun2 z3_mk_bvurem
 
 -- | Two's complement signed remainder (sign follows dividend).
 --
 -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga46c18a3042fca174fe659d3185693db1>
 mkBvsrem :: Context -> AST -> AST -> IO AST
-mkBvsrem = liftAst2 z3_mk_bvsrem
+mkBvsrem = liftFun2 z3_mk_bvsrem
 
 -- | Two's complement signed remainder (sign follows divisor).
 --
 -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga95dac8e6eecb50f63cb82038560e0879>
 mkBvsmod :: Context -> AST -> AST -> IO AST
-mkBvsmod = liftAst2 z3_mk_bvsmod
+mkBvsmod = liftFun2 z3_mk_bvsmod
 
 -- | Unsigned less than.
 --
 -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga5774b22e93abcaf9b594672af6c7c3c4>
 mkBvult :: Context -> AST -> AST -> IO AST
-mkBvult = liftAst2 z3_mk_bvult
+mkBvult = liftFun2 z3_mk_bvult
 
 -- | Two's complement signed less than.
 --
 -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga8ce08af4ed1fbdf08d4d6e63d171663a>
 mkBvslt :: Context -> AST -> AST -> IO AST
-mkBvslt = liftAst2 z3_mk_bvslt
+mkBvslt = liftFun2 z3_mk_bvslt
 
 -- | Unsigned less than or equal to.
 --
 -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gab738b89de0410e70c089d3ac9e696e87>
 mkBvule :: Context -> AST -> AST -> IO AST
-mkBvule = liftAst2 z3_mk_bvule
+mkBvule = liftFun2 z3_mk_bvule
 
 -- | Two's complement signed less than or equal to.
 --
 -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gab7c026feb93e7d2eab180e96f1e6255d>
 mkBvsle :: Context -> AST -> AST -> IO AST
-mkBvsle = liftAst2 z3_mk_bvsle
+mkBvsle = liftFun2 z3_mk_bvsle
 
 -- | Unsigned greater than or equal to.
 --
 -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gade58fbfcf61b67bf8c4a441490d3c4df>
 mkBvuge :: Context -> AST -> AST -> IO AST
-mkBvuge = liftAst2 z3_mk_bvuge
+mkBvuge = liftFun2 z3_mk_bvuge
 
 -- | Two's complement signed greater than or equal to.
 --
 -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaeec3414c0e8a90a6aa5a23af36bf6dc5>
 mkBvsge :: Context -> AST -> AST -> IO AST
-mkBvsge = liftAst2 z3_mk_bvsge
+mkBvsge = liftFun2 z3_mk_bvsge
 
 -- | Unsigned greater than.
 --
 -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga063ab9f16246c99e5c1c893613927ee3>
 mkBvugt :: Context -> AST -> AST -> IO AST
-mkBvugt = liftAst2 z3_mk_bvugt
+mkBvugt = liftFun2 z3_mk_bvugt
 
 -- | Two's complement signed greater than.
 --
 -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga4e93a985aa2a7812c7c11a2c65d7c5f0>
 mkBvsgt :: Context -> AST -> AST -> IO AST
-mkBvsgt = liftAst2 z3_mk_bvsgt
+mkBvsgt = liftFun2 z3_mk_bvsgt
 
 -- | Concatenate the given bit-vectors.
 --
 -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gae774128fa5e9ff7458a36bd10e6ca0fa>
 mkConcat :: Context -> AST -> AST -> IO AST
-mkConcat = liftAst2 z3_mk_concat
+mkConcat = liftFun2 z3_mk_concat
 
 -- | Extract the bits high down to low from a bitvector of size m to yield a new
 -- bitvector of size /n/, where /n = high - low + 1/.
 --
 -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga32d2fe7563f3e6b114c1b97b205d4317>
 mkExtract :: Context -> Int -> Int -> AST -> IO AST
-mkExtract c j i e
-  = checkError c $ AST <$> z3_mk_extract (unContext c) (fromIntegral j) (fromIntegral i) (unAST e)
+mkExtract = liftFun3 z3_mk_extract
 
 -- | Sign-extend of the given bit-vector to the (signed) equivalent bitvector
 -- of size /m+i/, where /m/ is the size of the given bit-vector.
 --
 -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gad29099270b36d0680bb54b560353c10e>
 mkSignExt :: Context -> Int -> AST -> IO AST
-mkSignExt = liftIntAst z3_mk_sign_ext
+mkSignExt = liftFun2 z3_mk_sign_ext
 
 -- | Extend the given bit-vector with zeros to the (unsigned) equivalent
 -- bitvector of size /m+i/, where /m/ is the size of the given bit-vector.
 --
 -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gac9322fae11365a78640baf9078c428b3>
 mkZeroExt :: Context -> Int -> AST -> IO AST
-mkZeroExt = liftIntAst z3_mk_zero_ext
+mkZeroExt = liftFun2 z3_mk_zero_ext
 
 -- | Repeat the given bit-vector up length /i/.
 --
 -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga03e81721502ea225c264d1f556c9119d>
 mkRepeat :: Context -> Int -> AST -> IO AST
-mkRepeat = liftIntAst z3_mk_repeat
+mkRepeat = liftFun2 z3_mk_repeat
 
 -- | Shift left.
 --
 -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gac8d5e776c786c1172fa0d7dfede454e1>
 mkBvshl :: Context -> AST -> AST -> IO AST
-mkBvshl = liftAst2 z3_mk_bvshl
+mkBvshl = liftFun2 z3_mk_bvshl
 
 -- | Logical shift right.
 --
 -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gac59645a6edadad79a201f417e4e0c512>
 mkBvlshr :: Context -> AST -> AST -> IO AST
-mkBvlshr = liftAst2 z3_mk_bvlshr
+mkBvlshr = liftFun2 z3_mk_bvlshr
 
 -- | Arithmetic shift right.
 --
 -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga674b580ad605ba1c2c9f9d3748be87c4>
 mkBvashr :: Context -> AST -> AST -> IO AST
-mkBvashr = liftAst2 z3_mk_bvashr
+mkBvashr = liftFun2 z3_mk_bvashr
 
 -- | Rotate bits of /t1/ to the left /i/ times.
 --
 -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga4932b7d08fea079dd903cd857a52dcda>
 mkRotateLeft :: Context -> Int -> AST -> IO AST
-mkRotateLeft = liftIntAst z3_mk_rotate_left
+mkRotateLeft = liftFun2 z3_mk_rotate_left
 
 -- | Rotate bits of /t1/ to the right /i/ times.
 --
 -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga3b94e1bf87ecd1a1858af8ebc1da4a1c>
 mkRotateRight :: Context -> Int -> AST -> IO AST
-mkRotateRight = liftIntAst z3_mk_rotate_right
+mkRotateRight = liftFun2 z3_mk_rotate_right
 
 -- | Rotate bits of /t1/ to the left /t2/ times.
 --
 -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaf46f1cb80e5a56044591a76e7c89e5e7>
 mkExtRotateLeft :: Context -> AST -> AST -> IO AST
-mkExtRotateLeft = liftAst2 z3_mk_ext_rotate_left
+mkExtRotateLeft = liftFun2 z3_mk_ext_rotate_left
 
 -- | Rotate bits of /t1/ to the right /t2/ times.
 --
 -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gabb227526c592b523879083f12aab281f>
 mkExtRotateRight :: Context -> AST -> AST -> IO AST
-mkExtRotateRight = liftAst2 z3_mk_ext_rotate_right
+mkExtRotateRight = liftFun2 z3_mk_ext_rotate_right
 
 -- | Create an /n/ bit bit-vector from the integer argument /t1/.
 --
 -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga35f89eb05df43fbd9cce7200cc1f30b5>
 mkInt2bv :: Context -> Int -> AST -> IO AST
-mkInt2bv c i e
-  = checkError c $ AST <$> z3_mk_int2bv (unContext c) (fromIntegral i) (unAST e)
+mkInt2bv = liftFun2 z3_mk_int2bv
 
 -- | Create an integer from the bit-vector argument /t1/. If /is_signed/ is false,
 -- then the bit-vector /t1/ is treated as unsigned. So the result is non-negative
 --
 -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gac87b227dc3821d57258d7f53a28323d4>
 mkBv2int :: Context -> AST -> Bool -> IO AST
-mkBv2int c e is_signed
-  = checkError c $ AST <$> z3_mk_bv2int (unContext c) (unAST e) (unBool is_signed)
+mkBv2int = liftFun2 z3_mk_bv2int
 
 -- | Create a predicate that checks that the bit-wise addition of /t1/ and /t2/
 -- does not overflow.
 --
 -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga88f6b5ec876f05e0d7ba51e96c4b077f>
 mkBvaddNoOverflow :: Context -> AST -> AST -> Bool -> IO AST
-mkBvaddNoOverflow c e1 e2 is_signed =
-  checkError c $ AST <$> z3_mk_bvadd_no_overflow (unContext c) (unAST e1) (unAST e2)
-                                                 (unBool is_signed)
+mkBvaddNoOverflow = liftFun3 z3_mk_bvadd_no_overflow
 
 -- | Create a predicate that checks that the bit-wise signed addition of /t1/
 -- and /t2/ does not underflow.
 --
 -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga1e2b1927cf4e50000c1600d47a152947>
 mkBvaddNoUnderflow :: Context -> AST -> AST -> IO AST
-mkBvaddNoUnderflow = liftAst2 z3_mk_bvadd_no_underflow
+mkBvaddNoUnderflow = liftFun2 z3_mk_bvadd_no_underflow
 
 -- | Create a predicate that checks that the bit-wise signed subtraction of /t1/
 -- and /t2/ does not overflow.
 --
 -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga785f8127b87e0b42130e6d8f52167d7c>
 mkBvsubNoOverflow :: Context -> AST -> AST -> IO AST
-mkBvsubNoOverflow = liftAst2 z3_mk_bvsub_no_overflow
+mkBvsubNoOverflow = liftFun2 z3_mk_bvsub_no_overflow
 
 -- | Create a predicate that checks that the bit-wise subtraction of /t1/ and
 -- /t2/ does not underflow.
 --
 -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga6480850f9fa01e14aea936c88ff184c4>
 mkBvsubNoUnderflow :: Context -> AST -> AST -> IO AST
-mkBvsubNoUnderflow = liftAst2 z3_mk_bvsub_no_underflow
+mkBvsubNoUnderflow = liftFun2 z3_mk_bvsub_no_underflow
 
 -- | Create a predicate that checks that the bit-wise signed division of /t1/
 -- and /t2/ does not overflow.
 --
 -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaa17e7b2c33dfe2abbd74d390927ae83e>
 mkBvsdivNoOverflow :: Context -> AST -> AST -> IO AST
-mkBvsdivNoOverflow = liftAst2 z3_mk_bvsdiv_no_overflow
+mkBvsdivNoOverflow = liftFun2 z3_mk_bvsdiv_no_overflow
 
 -- | Check that bit-wise negation does not overflow when /t1/ is interpreted as
 -- a signed bit-vector.
 --
 -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gae9c5d72605ddcd0e76657341eaccb6c7>
 mkBvnegNoOverflow :: Context -> AST -> IO AST
-mkBvnegNoOverflow = liftAst1 z3_mk_bvneg_no_overflow
+mkBvnegNoOverflow = liftFun1 z3_mk_bvneg_no_overflow
 
 -- | Create a predicate that checks that the bit-wise multiplication of /t1/ and
 -- /t2/ does not overflow.
 --
 -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga86f4415719d295a2f6845c70b3aaa1df>
 mkBvmulNoOverflow :: Context -> AST -> AST -> Bool -> IO AST
-mkBvmulNoOverflow c e1 e2 is_signed =
-  checkError c $ AST <$> z3_mk_bvmul_no_overflow (unContext c) (unAST e1) (unAST e2)
-                                                 (unBool is_signed)
+mkBvmulNoOverflow = liftFun3 z3_mk_bvmul_no_overflow
 
 -- | Create a predicate that checks that the bit-wise signed multiplication of
 -- /t1/ and /t2/ does not underflow.
 --
 -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga501ccc01d737aad3ede5699741717fda>
 mkBvmulNoUnderflow :: Context -> AST -> AST -> IO AST
-mkBvmulNoUnderflow = liftAst2 z3_mk_bvmul_no_underflow
+mkBvmulNoUnderflow = liftFun2 z3_mk_bvmul_no_underflow
 
 ---------------------------------------------------------------------
 -- Arrays
 --
 -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga38f423f3683379e7f597a7fe59eccb67>
 mkSelect :: Context -> AST -> AST -> IO AST
-mkSelect = liftAst2 z3_mk_select
+mkSelect = liftFun2 z3_mk_select
 
 -- | Array update.   
 --
 -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gae305a4f54b4a64f7e5973ae6ccb13593>
 mkStore :: Context -> AST -> AST -> AST -> IO AST
-mkStore c a1 a2 a3 = checkError c $ AST <$> z3_mk_store (unContext c) (unAST a1) (unAST a2) (unAST a3)
+mkStore = liftFun3 z3_mk_store
 
 -- | Create the constant array.
 --
 -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga84ea6f0c32b99c70033feaa8f00e8f2d>
 mkConstArray :: Context -> Sort -> AST -> IO AST
-mkConstArray c s a = checkError c $ AST <$> z3_mk_const_array (unContext c) (unSort s) (unAST a)
+mkConstArray = liftFun2 z3_mk_const_array
 
 -- | map f on the the argument arrays.
 --
 -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga9150242d9430a8c3d55d2ca3b9a4362d>
 mkMap :: Context -> FuncDecl -> Int -> [AST] -> IO AST
 mkMap c f n args = withArray (map unAST args) $ \args' ->
-    checkError c $ AST <$> z3_mk_map (unContext c) (unFuncDecl f) (fromIntegral n) args'
+    checkError c $ liftVal c =<< z3_mk_map (unContext c) (unFuncDecl f) (fromIntegral n) args'
 
 -- | Access the array default value. Produces the default range value, for
 -- arrays that can be represented as finite maps with a default range value.
 --
 -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga78e89cca82f0ab4d5f4e662e5e5fba7d>
 mkArrayDefault :: Context -> AST -> IO AST
-mkArrayDefault = liftAst1 z3_mk_array_default
+mkArrayDefault = liftFun1 z3_mk_array_default
 
 -- TODO Sets
 
 --
 -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gac8aca397e32ca33618d8024bff32948c>
 mkNumeral :: Context -> String -> Sort -> IO AST
-mkNumeral c str s =
-  withCString str $ \cstr->
-    checkError c $ AST <$> z3_mk_numeral (unContext c) cstr (unSort s)
+mkNumeral = liftFun2 z3_mk_numeral
 
 -------------------------------------------------
 -- Numerals / Integers
 
 {-# INLINE mkIntZ3 #-}
 mkIntZ3 :: Context -> Int32 -> Sort -> IO AST
-mkIntZ3 c n s = checkError c $ AST <$> z3_mk_int (unContext c) cn (unSort s)
-  where cn = fromIntegral n :: CInt
+mkIntZ3 c n s = marshal z3_mk_int c $ withVal s . withIntegral n
 
 {-# INLINE mkUnsignedIntZ3 #-}
 mkUnsignedIntZ3 :: Context -> Word32 -> Sort -> IO AST
-mkUnsignedIntZ3 c n s = checkError c $ AST <$> z3_mk_unsigned_int (unContext c) cn (unSort s)
-  where cn = fromIntegral n :: CUInt
+mkUnsignedIntZ3 c n s = marshal z3_mk_unsigned_int c $
+  withVal s . withIntegral n
 
 {-# INLINE mkInt64Z3 #-}
 mkInt64Z3 :: Context -> Int64 -> Sort -> IO AST
-mkInt64Z3 c n s = checkError c $ AST <$> z3_mk_int64 (unContext c) cn (unSort s)
-  where cn = fromIntegral n :: CLLong
+mkInt64Z3 = liftFun2 z3_mk_int64
 
 {-# INLINE mkUnsignedInt64Z3 #-}
 mkUnsignedInt64Z3 :: Context -> Word64 -> Sort -> IO AST
-mkUnsignedInt64Z3 c n s =
-  checkError c $ AST <$> z3_mk_unsigned_int64 (unContext c) cn (unSort s)
-  where cn = fromIntegral n :: CULLong
+mkUnsignedInt64Z3 = liftFun2 z3_mk_unsigned_int64
 
 {-# RULES "mkInt/mkInt_IntZ3" mkInt = mkInt_IntZ3 #-}
 mkInt_IntZ3 :: Context -> Int32 -> IO AST
 
 {-# RULES "mkReal/mkRealZ3" mkReal = mkRealZ3 #-}
 mkRealZ3 :: Context -> Ratio Int32 -> IO AST
-mkRealZ3 c r = checkError c $ AST <$> z3_mk_real (unContext c) n d
+mkRealZ3 c r = checkError c $ liftVal c =<< z3_mk_real (unContext c) n d
   where n = (fromIntegral $ numerator r)   :: CInt
         d = (fromIntegral $ denominator r) :: CInt
 
 
 mkPattern :: Context -> [AST] -> IO Pattern
 mkPattern _ [] = error "Z3.Base.mkPattern: empty list of expressions"
-mkPattern c es =
-  withArray (map unAST es) $ \aptr ->
-    checkError c $ Pattern <$> z3_mk_pattern (unContext c) n aptr
-  where n = genericLength es
+mkPattern c es = marshal z3_mk_pattern c $ withAstArray es
 
 mkBound :: Context -> Int -> Sort -> IO AST
 mkBound c i s
-  | i >= 0    = checkError c $ AST <$> z3_mk_bound (unContext c) (fromIntegral i) (unSort s)
+  | i >= 0    = liftFun2 z3_mk_bound c i s
   | otherwise = error "Z3.Base.mkBound: negative de-Bruijn index"
 
 mkForall :: Context -> [Pattern] -> [Symbol] -> [Sort] -> AST -> IO AST
   = withArray (map unPattern pats) $ \patsPtr ->
     withArray (map unSymbol  x   ) $ \xptr ->
     withArray (map unSort    s   ) $ \sptr ->
-      checkError c $ AST <$> z3_mk_forall cptr 0 n patsPtr len sptr xptr (unAST p)
+      checkError c $ liftVal c =<< z3_mk_forall cptr 0 n patsPtr len sptr xptr (unAST p)
   where n    = genericLength pats
         cptr = unContext c
         len
 mkForallConst c pats apps p
   = withArray (map unPattern pats) $ \patsPtr ->
     withArray (map unApp     apps) $ \appsPtr ->
-      checkError c $ AST <$>
+      checkError c $ liftVal c =<<
         z3_mk_forall_const cptr 0 len appsPtr n patsPtr (unAST p)
   where n    = genericLength pats
         cptr = unContext c
 --
 -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga8fc3550edace7bc046e16d1f96ddb419>
 getBvSortSize :: Context -> Sort -> IO Int
-getBvSortSize c s =
-  checkError c $ fromIntegral <$> z3_get_bv_sort_size (unContext c) (unSort s)
+getBvSortSize = liftFun1 z3_get_bv_sort_size
 
 -- | Return the sort of an AST node.
 --
 -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga0a4dac7e9397ff067136354cd33cb933>
 getSort :: Context -> AST -> IO Sort
-getSort c e = checkError c $ Sort <$> z3_get_sort (unContext c) (unAST e)
+getSort = liftFun1 z3_get_sort
 
 -- | Cast a 'Z3_lbool' from Z3.Base.C to @Bool@.
 castLBool :: Z3_lbool -> Maybe Bool
 --
 -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga94617ef18fa7157e1a3f85db625d2f4b>
 getNumeralString :: Context -> AST -> IO String
-getNumeralString c a = checkError c $ peekCString =<< z3_get_numeral_string ctxPtr (unAST a)
-  where ctxPtr = unContext c
+getNumeralString = liftFun1 z3_get_numeral_string
 
 -- | Return 'Z3Int' value
 getInt :: Context -> AST -> IO Integer
 --
 -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaf9345fd0822d7e9928dd4ab14a09765b>
 toApp :: Context -> AST -> IO App
-toApp c a = checkError c $ App <$> z3_to_app (unContext c) (unAST a)
+toApp = liftFun1 z3_to_app
 
 -- TODO Modifiers
 
 --
 -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga7d9262dc6e79f2aeb23fd4a383589dda>
 getAsArrayFuncDecl :: Context -> AST -> IO FuncDecl
-getAsArrayFuncDecl ctx a = checkError ctx $
-  FuncDecl <$> z3_get_as_array_func_decl (unContext ctx) (unAST a)
+getAsArrayFuncDecl = liftFun1 z3_get_as_array_func_decl
 
 -- | The (_ as-array f) AST node is a construct for assigning interpretations
 -- for arrays in Z3. It is the array such that forall indices i we have that
 --
 -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga4674da67d226bfb16861829b9f129cfa>
 isAsArray :: Context -> AST -> IO Bool
-isAsArray ctx a = toBool <$> z3_is_as_array (unContext ctx) (unAST a)
+isAsArray = liftFun1 z3_is_as_array
 
 
 getMapFromInterp :: Context -> FuncInterp -> IO [([AST], AST)]
 --
 -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga2bab9ae1444940e7593729beec279844>
 funcInterpGetNumEntries :: Context -> FuncInterp -> IO Int
-funcInterpGetNumEntries ctx fi = checkError ctx $ fromIntegral <$>
-  z3_func_interp_get_num_entries (unContext ctx) (unFuncInterp fi)
+funcInterpGetNumEntries = liftFun1 z3_func_interp_get_num_entries
 
 -- | Return a _point_ of the given function intepretation.
 -- It represents the value of f in a particular point.
 --
 -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaf157e1e1cd8c0cfe6a21be6370f659da>
 funcInterpGetEntry :: Context -> FuncInterp -> Int -> IO FuncEntry
-funcInterpGetEntry ctx fi i = checkError ctx $ FuncEntry <$>
-  z3_func_interp_get_entry (unContext ctx) (unFuncInterp fi) (fromIntegral i)
+funcInterpGetEntry = liftFun2 z3_func_interp_get_entry
 
 -- | Return the 'else' value of the given function interpretation.
 --
 -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga46de7559826ba71b8488d727cba1fb64>
 funcInterpGetElse :: Context -> FuncInterp -> IO AST
-funcInterpGetElse ctx fi = checkError ctx $
-  AST <$> z3_func_interp_get_else (unContext ctx) (unFuncInterp fi)
+funcInterpGetElse = liftFun1 z3_func_interp_get_else
 
 -- | Return the arity (number of arguments) of the given function
 -- interpretation.
 --
 -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaca22cbdb6f7787aaae5d814f2ab383d8>
 funcInterpGetArity :: Context -> FuncInterp -> IO Int
-funcInterpGetArity ctx fi = checkError ctx $
-  fromIntegral <$> z3_func_interp_get_arity (unContext ctx) (unFuncInterp fi)
+funcInterpGetArity = liftFun1 z3_func_interp_get_arity
 
 -- | Return the value of this point.
 --
 -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga9fd65e2ab039aa8e40608c2ecf7084da>
 funcEntryGetValue :: Context -> FuncEntry -> IO AST
-funcEntryGetValue ctx entry = checkError ctx $
-  AST <$> z3_func_entry_get_value (unContext ctx) (unFuncEntry entry)
+funcEntryGetValue = liftFun1 z3_func_entry_get_value
 
 -- | Return the number of arguments in a Z3_func_entry object.
 --
 -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga51aed8c5bc4b1f53f0c371312de3ce1a>
 funcEntryGetNumArgs :: Context -> FuncEntry -> IO Int
-funcEntryGetNumArgs ctx entry = checkError ctx $ fromIntegral <$>
-  z3_func_entry_get_num_args (unContext ctx) (unFuncEntry entry)
+funcEntryGetNumArgs = liftFun1 z3_func_entry_get_num_args
 
 -- | Return an argument of a Z3_func_entry object.
 --
 -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga6fe03fe3c824fceb52766a4d8c2cbeab>
 funcEntryGetArg :: Context -> FuncEntry -> Int -> IO AST
-funcEntryGetArg ctx entry i = checkError ctx $ AST <$>
-  z3_func_entry_get_arg (unContext ctx) (unFuncEntry entry) (fromIntegral i)
+funcEntryGetArg = liftFun2 z3_func_entry_get_arg
 
 -- | Convert the given model into a string.
 --
 -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaf36d49862a8c0d20dd5e6508eef5f8af>
 modelToString :: Context -> Model -> IO String
-modelToString c m = checkError c $
-  z3_model_to_string (unContext c) (unModel m) >>= peekCString
+modelToString = liftFun1 z3_model_to_string
 
 -- | Alias for 'modelToString'.
 showModel :: Context -> Model -> IO String
 --
 -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gad651ad68c7a060cbb5616349233cb10f>
 push :: Context -> IO ()
-push c = checkError c $ z3_push $ unContext c
+push = liftFun0 z3_push
 
 -- | Backtrack /n/ backtracking points.
 --
 -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gab2b3a542006c86c8d86dc37872f88b61>
 pop :: Context -> Int -> IO ()
-pop ctx cnt = checkError ctx $ z3_pop (unContext ctx) $ fromIntegral cnt
+pop = liftFun1 z3_pop
 
 -- TODO Constraints: Z3_get_num_scopes
 
 --
 -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga1a05ff73a564ae7256a2257048a4680a>
 assertCnstr :: Context -> AST -> IO ()
-assertCnstr ctx ast = checkError ctx $
-  z3_assert_cnstr (unContext ctx) (unAST ast)
+assertCnstr = liftFun1 z3_assert_cnstr
 
 -- | Get model (logical context is consistent)
 --
 --
 -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga0cc98d3ce68047f873e119bccaabdbee>
 delModel :: Context -> Model -> IO ()
-delModel c m = checkError c $ z3_del_model (unContext c) (unModel m)
+delModel = liftFun1 z3_del_model
 
 -- | Check whether the given logical context is consistent or not.
 --
 -- * Parameters
 
 mkParams :: Context -> IO Params
-mkParams c = checkError c $ Params <$> z3_mk_params (unContext c)
+mkParams = liftFun0 z3_mk_params
 
 paramsSetBool :: Context -> Params -> Symbol -> Bool -> IO ()
-paramsSetBool c params sym b = checkError c $
-  z3_params_set_bool (unContext c) (unParams params) (unSymbol sym) (unBool b)
+paramsSetBool = liftFun3 z3_params_set_bool
 
 paramsSetUInt :: Context -> Params -> Symbol -> Int -> IO ()
-paramsSetUInt c params sym v = checkError c $
-  z3_params_set_uint (unContext c) (unParams params)
-        (unSymbol sym) (fromIntegral v)
+paramsSetUInt = liftFun3 z3_params_set_uint
 
 paramsSetDouble :: Context -> Params -> Symbol -> Double -> IO ()
-paramsSetDouble c params sym v = checkError c $
-  z3_params_set_double (unContext c) (unParams params)
-        (unSymbol sym) (realToFrac v)
+paramsSetDouble = liftFun3 z3_params_set_double
 
 paramsSetSymbol :: Context -> Params -> Symbol -> Symbol -> IO ()
-paramsSetSymbol c params sym v =
-  checkError c $ z3_params_set_symbol (unContext c) (unParams params) (unSymbol sym)
-                                      (unSymbol v)
+paramsSetSymbol = liftFun3 z3_params_set_symbol
 
 paramsToString :: Context -> Params -> IO String
-paramsToString c (Params params) =
-  checkError c (z3_params_to_string (unContext c) params) >>= peekCString
+paramsToString = liftFun1 z3_params_to_string
 
 
 ---------------------------------------------------------------------
   where cPtr = unContext c
 
 mkSolver :: Context -> IO Solver
-mkSolver c = checkError c (mkSolverForeign c =<< z3_mk_solver cPtr)
-  where cPtr = unContext c
+mkSolver = liftFun0 z3_mk_solver
 
 mkSimpleSolver :: Context -> IO Solver
-mkSimpleSolver c = checkError c $ mkSolverForeign c =<< z3_mk_simple_solver (unContext c)
+mkSimpleSolver = liftFun0 z3_mk_simple_solver
 
 mkSolverForLogic :: Context -> Logic -> IO Solver
 mkSolverForLogic c logic =
        mkSolverForeign c =<< z3_mk_solver_for_logic (unContext c) (unSymbol sym)
 
 solverSetParams :: Context -> Solver -> Params -> IO ()
-solverSetParams c solver params = checkError c $
-  withSolverPtr solver $ \solv ->
-    z3_solver_set_params (unContext c) solv (unParams params)
+solverSetParams = liftFun2 z3_solver_set_params
 
 solverPush :: Context -> Solver -> IO ()
-solverPush c solver = checkError c $
-  withSolverPtr solver (z3_solver_push (unContext c))
+solverPush = liftFun1 z3_solver_push
 
 solverPop :: Context -> Solver -> Int -> IO ()
-solverPop c solver i = checkError c $
-  withSolverPtr solver $ \solv ->
-    z3_solver_pop (unContext c) solv (fromIntegral i)
+solverPop = liftFun2 z3_solver_pop
 
 solverReset :: Context -> Solver -> IO ()
-solverReset c solver = checkError c $
-  withSolverPtr solver (z3_solver_reset (unContext c))
+solverReset = liftFun1 z3_solver_reset
 
 -- | Number of backtracking points.
 --
 -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gafd4b4a6465601835341b477b75725b28>
 solverGetNumScopes :: Context -> Solver -> IO Int
-solverGetNumScopes ctx solver = fmap fromIntegral $
-  withSolverPtr solver (z3_solver_get_num_scopes (unContext ctx))
+solverGetNumScopes = liftFun1 z3_solver_get_num_scopes
 
 solverAssertCnstr :: Context -> Solver -> AST -> IO ()
-solverAssertCnstr c solver ast = checkError c $
-  withSolverPtr solver $ \solv ->
-                 z3_solver_assert (unContext c) solv (unAST ast)
+solverAssertCnstr = liftFun2 z3_solver_assert
 
 solverAssertAndTrack :: Context -> Solver -> AST -> AST -> IO ()
-solverAssertAndTrack c solver constraint var =
-  checkError c $ withSolverPtr solver $ \solv ->
-    z3_solver_assert_and_track (unContext c)
-                               solv
-                               (unAST constraint)
-                               (unAST var)
+solverAssertAndTrack = liftFun3 z3_solver_assert_and_track
 
 solverCheck :: Context -> Solver -> IO Result
 solverCheck c solver = checkError c $ fmap toResult $
   where cptr = unContext c
 
 solverGetReasonUnknown :: Context -> Solver -> IO String
-solverGetReasonUnknown c solver = checkError c $
-  withSolverPtr solver (z3_solver_get_reason_unknown (unContext c))
-    >>= peekCString
-
+solverGetReasonUnknown = liftFun1 z3_solver_get_reason_unknown
 
 -- | Convert the given solver into a string.
 --
 -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaf52e41db4b12a84188b80255454d3abb>
 solverToString :: Context -> Solver -> IO String
-solverToString ctx solver = checkError ctx $
-  (withSolverPtr solver (z3_solver_to_string (unContext ctx))) >>= peekCString
+solverToString = liftFun1 z3_solver_to_string
 
 ---------------------------------------------------------------------
 -- String Conversion
 
 -- | Convert an AST to a string.
 astToString :: Context -> AST -> IO String
-astToString ctx ast =
-  checkError ctx $ z3_ast_to_string (unContext ctx) (unAST ast) >>= peekCString
+astToString = liftFun1 z3_ast_to_string
 
 -- | Convert a pattern to a string.
 patternToString :: Context -> Pattern -> IO String
-patternToString ctx pattern =
-  checkError ctx $ z3_pattern_to_string (unContext ctx) (unPattern pattern) >>= peekCString
+patternToString = liftFun1 z3_pattern_to_string
 
 -- | Convert a sort to a string.
 sortToString :: Context -> Sort -> IO String
-sortToString ctx sort =
-  checkError ctx $ z3_sort_to_string (unContext ctx) (unSort sort) >>= peekCString
+sortToString = liftFun1 z3_sort_to_string
 
 -- | Convert a FuncDecl to a string.
 funcDeclToString :: Context -> FuncDecl -> IO String
-funcDeclToString ctx funcDecl =
-  checkError ctx $ z3_func_decl_to_string (unContext ctx) (unFuncDecl funcDecl) >>= peekCString
+funcDeclToString = liftFun1 z3_func_decl_to_string
 
 -- | Convert the given benchmark into SMT-LIB formatted string.
 --
   withCString logic $ \clogic ->
   withCString st $ \cst ->
   withCString attr $ \cattr ->
-  withArray (map unAST assump) $ \cassump ->
+  withAstArray assump $ \numAssump cassump -> liftVal c =<<
     z3_benchmark_to_smtlib_string (unContext c) cname clogic cst cattr
                                   numAssump cassump (unAST f)
-      >>= peekCString
-  where numAssump = genericLength assump
 
 ---------------------------------------------------------------------
 -- Lifting
 
-liftAst1 :: (Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast))
-              -> Context -> AST -> IO AST
-liftAst1 f c e = checkError c $
-  AST <$> f (unContext c) (unAST e)
-{-# INLINE liftAst1 #-}
+withIntegral :: (Integral a, Integral b) => a -> (b -> r) -> r
+withIntegral x f = f (fromIntegral x)
 
-liftAst2 :: (Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast))
-              -> Context -> AST -> AST -> IO AST
-liftAst2 f c e1 e2 = checkError c $
-  AST <$> f (unContext c) (unAST e1) (unAST e2)
-{-# INLINE liftAst2 #-}
+withAstArray :: [AST] -> (CUInt -> Ptr (Ptr Z3_ast) -> IO a) -> IO a
+withAstArray as f = withArrayLen (map unAST as) $ \n -> f (fromIntegral n)
+{-# INLINE withAstArray #-}
 
 liftAstN :: String
             -> (Ptr Z3_context -> CUInt -> Ptr (Ptr Z3_ast) -> IO (Ptr Z3_ast))
             -> Context -> [AST] -> IO AST
 liftAstN s _ _ [] = error s
-liftAstN _ f c es =
-  withArray (map unAST es) $ \aptr ->
-    checkError c $
-      AST <$> f (unContext c) n aptr
-  where n = genericLength es
+liftAstN _ f c es = marshal f c $ withAstArray es
 {-# INLINE liftAstN #-}
 
-liftIntAst :: (Ptr Z3_context -> CUInt-> Ptr Z3_ast -> IO (Ptr Z3_ast))
-              -> Context -> Int -> AST -> IO AST
-liftIntAst f c i e = checkError c $
-  AST <$> f (unContext c) (fromIntegral i) (unAST e)
-{-# INLINE liftIntAst #-}
+class LiftVal a where
+  type Lifted a :: *
+  liftVal :: Context -> a -> IO (Lifted a)
+  withVal :: Lifted a -> (a -> IO b) -> IO b
+
+instance LiftVal () where
+  type Lifted () = ()
+  liftVal _ = return
+  withVal x f = f x
+
+instance LiftVal Z3_bool where
+  type Lifted Z3_bool = Bool
+  liftVal _ = return . toBool
+  withVal b f = f (unBool b)
+
+instance LiftVal CUInt where
+  type Lifted CUInt = Int
+  liftVal _ = return . fromIntegral
+  withVal i f = f (fromIntegral i)
+
+instance LiftVal CLLong where
+  type Lifted CLLong = Int64
+  liftVal _ = return . fromIntegral
+  withVal i f = f (fromIntegral i)
+
+instance LiftVal CULLong where
+  type Lifted CULLong = Word64
+  liftVal _ = return . fromIntegral
+  withVal i f = f (fromIntegral i)
+
+instance LiftVal CDouble where
+  type Lifted CDouble = Double
+  liftVal _ = return . realToFrac
+  withVal d f = f (realToFrac d)
+
+instance LiftVal CString where
+  type Lifted CString = String
+  liftVal _ = peekCString
+  withVal   = withCString
+
+instance LiftVal (Ptr Z3_app) where
+  type Lifted (Ptr Z3_app) = App
+  liftVal _ = return . App
+  withVal a f = f (unApp a)
+
+instance LiftVal (Ptr Z3_params) where
+  type Lifted (Ptr Z3_params) = Params
+  liftVal _ = return . Params
+  withVal p f = f (unParams p)
+
+instance LiftVal (Ptr Z3_symbol) where
+  type Lifted (Ptr Z3_symbol) = Symbol
+  liftVal _ = return . Symbol
+  withVal s f = f (unSymbol s)
+
+instance LiftVal (Ptr Z3_ast) where
+  type Lifted (Ptr Z3_ast) = AST
+  liftVal _ = return . AST
+  withVal a f = f (unAST a)
+
+instance LiftVal (Ptr Z3_sort) where
+  type Lifted (Ptr Z3_sort) = Sort
+  liftVal _ = return . Sort
+  withVal a f = f (unSort a)
+
+instance LiftVal (Ptr Z3_func_decl) where
+  type Lifted (Ptr Z3_func_decl) = FuncDecl
+  liftVal _ = return . FuncDecl
+  withVal a f = f (unFuncDecl a)
+
+instance LiftVal (Ptr Z3_func_entry) where
+  type Lifted (Ptr Z3_func_entry) = FuncEntry
+  liftVal _ = return . FuncEntry
+  withVal e f = f (unFuncEntry e)
+
+instance LiftVal (Ptr Z3_func_interp) where
+  type Lifted (Ptr Z3_func_interp) = FuncInterp
+  liftVal _ = return . FuncInterp
+  withVal a f = f (unFuncInterp a)
+
+instance LiftVal (Ptr Z3_model) where
+  type Lifted (Ptr Z3_model) = Model
+  liftVal _ = return . Model
+  withVal m f = f (unModel m)
+
+instance LiftVal (Ptr Z3_pattern) where
+  type Lifted (Ptr Z3_pattern) = Pattern
+  liftVal _ = return . Pattern
+  withVal a f = f (unPattern a)
+
+instance LiftVal (Ptr Z3_solver) where
+  type Lifted (Ptr Z3_solver) = Solver
+  liftVal = mkSolverForeign
+  withVal = withSolverPtr
+
+marshal :: LiftVal r => (Ptr Z3_context -> t)
+                       -> Context -> (t -> IO r) -> IO (Lifted r)
+marshal f c cont = checkError c $ cont (f (unContext c)) >>= liftVal c
+
+liftFun0 :: LiftVal r => (Ptr Z3_context -> IO r) ->
+              Context -> IO (Lifted r)
+liftFun0 f c = checkError c $ liftVal c =<< f (unContext c)
+{-# INLINE liftFun0 #-}
+
+liftFun1 :: (LiftVal a, LiftVal r) => (Ptr Z3_context -> a -> IO r) ->
+              Context -> Lifted a -> IO (Lifted r)
+liftFun1 f c x = checkError c $ withVal x $ \a ->
+  liftVal c =<< f (unContext c) a
+{-# INLINE liftFun1 #-}
+
+liftFun2 :: (LiftVal a, LiftVal b, LiftVal r) =>
+              (Ptr Z3_context -> a -> b -> IO r) ->
+              Context -> Lifted a -> Lifted b -> IO (Lifted r)
+liftFun2 f c x y = checkError c $ withVal x $ \a -> withVal y $ \b ->
+  liftVal c =<< f (unContext c) a b
+{-# INLINE liftFun2 #-}
+
+liftFun3 :: (LiftVal a, LiftVal b, LiftVal c, LiftVal r) =>
+              (Ptr Z3_context -> a -> b -> c -> IO r) ->
+              Context -> Lifted a -> Lifted b -> Lifted c -> IO (Lifted r)
+liftFun3 f c x y z = checkError c $
+  withVal x $ \x1 -> withVal y $ \y1 -> withVal z $ \z1 ->
+    liftVal c =<< f (unContext c) x1 y1 z1
+{-# INLINE liftFun3 #-}
 
 ---------------------------------------------------------------------
 -- Utils