diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,24 @@
+Copyright (c) 2014, Tobias Gödderz
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are met:
+    * Redistributions of source code must retain the above copyright
+      notice, this list of conditions and the following disclaimer.
+    * Redistributions in binary form must reproduce the above copyright
+      notice, this list of conditions and the following disclaimer in the
+      documentation and/or other materials provided with the distribution.
+    * Neither the name of the University of Bonn nor the names of its
+      contributors may be used to endorse or promote products derived from this
+      software without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND
+ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED
+WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
+DISCLAIMED. IN NO EVENT SHALL TOBIAS GÖDDERZ BE LIABLE FOR ANY DIRECT,
+INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
+BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF
+LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE
+OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF
+ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
diff --git a/Setup.hs b/Setup.hs
new file mode 100644
--- /dev/null
+++ b/Setup.hs
@@ -0,0 +1,2 @@
+import Distribution.Simple
+main = defaultMain
diff --git a/Test/OITestGenerator.hs b/Test/OITestGenerator.hs
new file mode 100644
--- /dev/null
+++ b/Test/OITestGenerator.hs
@@ -0,0 +1,361 @@
+{-# LANGUAGE TemplateHaskell #-}
+
+module Test.OITestGenerator (
+    AxiomResult, (===>), (=!=),
+    Axiom, axiom,
+    Arg, Op, op, arg, but, only, withConstraint,
+    withGens,
+    generate_oi_tests, generate_axiom's_tests, generate_single_test,
+    generate_basic_tests,
+    show_all_tests,
+) where
+
+import Control.Applicative
+import Control.Monad
+import Data.List
+import Language.Haskell.TH
+import Prelude hiding (exp)
+import Test.OITestGenerator.Axiom
+import Test.OITestGenerator.GenHelper
+import Test.OITestGenerator.Op
+import Test.OITestGenerator.OpArg
+import Test.QuickCheck
+
+{- Functions to export -}
+
+-- | Derives one test from each 'Axiom' by translating it to a QuickCheck
+-- 'Property'. This is done basically by replacing '=!=' with '==' and '===>'
+-- with 'QuickCheck.==>'.
+--
+-- It returns an expression of type @[Property]@, i.e.
+--
+-- > $(generate_basic_tests axs) :: [Property]
+generate_basic_tests :: [Axiom] -> ExpQ
+generate_basic_tests = liftM ListE . mapM gen_basic_test
+
+-- | Generate all operation invariance tests that typecheck. For example, given
+-- an operation
+--
+-- > f :: A -> A -> B -> C
+--
+-- and an axiom
+--
+-- > ax :: D -> AxiomResult A
+-- > ax x = lhs x =!= rhs x
+--
+-- the following tests are generated:
+--
+-- > property $ \y2 y3 -> f (lhs x) y2 y3 == f (rhs x) y2 y3
+-- > property $ \y1 y3 -> f y1 (lhs x) y3 == f y1 (rhs x) y3
+--
+-- but not
+--
+-- > property $ \y1 y2 -> f y1 y2 (lhs x) == f y1 y2 (rhs x)
+--
+-- because of the types.
+--
+-- All combinations of operations, their respective arguments and axioms are tried.
+--
+-- It returns an expression of type @[Property]@, i.e.
+--
+-- > $(generate_oi_tests axs ops) :: [Property]
+generate_oi_tests :: [Axiom] -> [Op] -> ExpQ
+generate_oi_tests = gen_tests
+
+-- | A convenience function for calling 'generate_oi_tests' with only one axiom.
+--
+-- It returns an expression of type @[Property]@, i.e.
+--
+-- > $(generate_axiom's_tests ax ops) :: [Property]
+generate_axiom's_tests :: Axiom -> [Op] -> ExpQ
+generate_axiom's_tests ax = gen_tests [ax]
+
+-- | Calls 'generate_oi_tests' with only the given 'Axiom' and 'Op'. It checks
+-- if there is exactly one test that can be generated and throws an error
+-- otherwise. If multiple applications of the given operation to the given
+-- axioms are possible (i.e. it has multiple arguments with a matching type),
+-- the allowed arguments have to be restricted using 'but' or 'only'.
+--
+-- It returns an expression of type @Property@, i.e.
+--
+-- > $(generate_single_test ax op) :: Property
+generate_single_test :: Axiom -> Op -> ExpQ
+generate_single_test ax opn = op2opArgs opn
+    >>= filter_Ops ax
+    >>= \args ->
+        case args of
+            [op_arg] -> generate_test ax op_arg
+            _        -> do let axnm = axiom_name ax
+                           let opnm = op_name opn
+                           axtp <- return_type_of_axiom axnm
+                           opargs <- op_args opn
+                           oparg_types <- liftM (zip opargs) $ mapM (flip type_of_argi opnm) opargs
+                           fail $ "Invalid number of feasible Op arguments. "
+                            ++ "Expected 1, but got " ++ show (length args)
+                            ++ ( if (length args) == 0
+                                 then ""
+                                 else ", namely " ++ show (map opArg_argi args)
+                               )
+                            ++ "."
+                            ++ "\n"
+                            ++ "Type of axiom " ++ show axnm ++ "'s result:\n"
+                            ++ "         " ++ pprint axtp ++ "\n"
+                            ++ "Type of operation arguments " ++ show opnm ++ ":\n"
+                            ++ (concatMap (\(i,tp) -> "  Arg#" ++ show i ++ ": " ++ pprint tp ++ "\n") oparg_types) ++ "\n" 
+
+-- | @show_all_tests Nothing axs ops@ returns a 'String' typed expression. Print
+-- the resulting string to get a piece of code, containing one property for each
+-- possible operation invariance test, defined via 'generate_single_test'.
+--
+-- The first argument can replace the default function generating a name for
+-- each test, which is
+--
+-- > \opn argi ax -> opn ++ show argi ++ "_" ++ ax
+--
+-- . An example output looks like this:
+--
+-- > enqueue1_q3 :: Property
+-- > enqueue1_q3 = $(generate_single_test (axiom 'q3) (op 'enqueue `only` 1))
+show_all_tests :: Maybe (String -> Int -> String -> String) -> [Name] -> [Name] -> ExpQ
+show_all_tests Nothing axs ops = show_all_tests (Just def_test_name) axs ops
+show_all_tests (Just fun) axs ops =
+    cross_ops_axs ops axs
+    >>= return . concatMap (\(opn, argi, ax) ->
+        let name = fun (nameBase opn) argi (nameBase ax)
+        in  name ++ " :: Property\n" ++
+            name ++ " = " ++ "$(" ++ intercalate " "
+            ["generate_single_test",
+            "(axiom '" ++ nameBase ax ++ ")",
+            "(op '" ++ nameBase opn ++ " `only` " ++ show argi ++ ")"]
+            ++ ")\n\n"
+    )
+    >>= stringE
+
+{- Private functions -}
+
+simple_dec :: String -> Exp -> Dec
+simple_dec nm exp = ValD (VarP (mkName nm)) (NormalB exp) []
+
+def_test_name :: String -> Int -> String -> String
+def_test_name opn argi ax = opn ++ show argi ++ "_" ++ ax
+
+gen_label :: Int -> Name -> Name -> String
+gen_label argi opn ax = show opn ++ "@" ++ show argi ++ "/" ++ show ax
+
+concatMapM :: (Monad m) => (a -> m [b]) -> [a] -> m [b]
+concatMapM f = liftM concat . mapM f
+
+(.>) :: (a -> b) -> (b -> c) -> a -> c
+(.>) = flip (.)
+
+gen_tests_per_ax :: Axiom -> [Op] -> Q [Exp]
+gen_tests_per_ax ax ops =
+        cross_Ops_args ops
+        >>= filter_Ops ax
+        >>= mapM (generate_test ax)
+
+gen_tests :: [Axiom] -> [Op] -> ExpQ
+gen_tests axs ops = concatMapM (flip gen_tests_per_ax ops) axs
+                    >>= return . ListE
+
+cross_ops_axs :: [Name] -> [Name] -> Q [(Name, Int, Name)]
+cross_ops_axs ops axs = concatMapM (\ax
+    -> cross_ops_args ops
+    >>= filter_ops ax
+    >>= mapM (\(argi, opn) -> return (opn, argi, ax))
+    ) axs
+
+cross_ops_args :: [Name] -> Q [(Int, Name)]
+cross_ops_args = concatMapM cross_op_args
+
+cross_op_args :: Name -> Q [(Int, Name)]
+cross_op_args opn = typeof opn >>= \tp -> return $ zip (enumFromTo 1 $ num_args tp) (repeat opn)
+
+cross_Ops_args :: [Op] -> Q [OpArg]
+cross_Ops_args = concatMapM cross_Op_args
+
+cross_Op_args :: Op -> Q [OpArg]
+cross_Op_args = op2opArgs
+
+delete_i :: Int -> [a] -> [a]
+delete_i i xs = take i xs ++ drop (i+1) xs
+
+apply_gens_to' :: ExpQ -> [Name] -> Int -> ExpQ
+apply_gens_to' prop [] _ = prop
+apply_gens_to' prop (x:xs) n = [| $app (forAll $(varE x)) $(apply_gens_to' prop xs (n+1)) |]
+    where app = liftAn n
+
+apply_gens_to :: ExpQ -> [Name] -> ExpQ
+apply_gens_to prop xs = apply_gens_to' prop xs 0
+
+gen_basic_test :: Axiom -> ExpQ
+gen_basic_test ax =
+    let axnm        = axiom_name ax
+        test_name   = show axnm
+        axE         = varE axnm
+        app         = num_args_name axnm >>= liftAn
+        app2        = num_args_name axnm >>= liftA2n
+    in [|
+            let  lhs         = $app ar_lhs   $axE
+                 rhs         = $app ar_rhs   $axE
+                 axiom_cond  = $app ar_cond  $axE
+            in  label test_name $ property $
+                $app2 (==>) axiom_cond $
+                $app2 (==) lhs rhs
+        |]
+
+generate_test :: Axiom -> OpArg -> ExpQ
+generate_test ax opn =
+    do
+        let axnm = axiom_name ax
+        let opnm = opArg_name opn
+        let argi = opArg_argi opn
+        argn_ax <- num_args_name axnm
+        argn_op <- num_args_name opnm
+        let axE = varE axnm
+        let opE = varE opnm
+        ax_custom_gens <- axiom_gens ax
+        let op_custom_gens = opArg_gens opn
+        let ax_gens = if length ax_custom_gens > 0
+                      then ax_custom_gens
+                      else replicate argn_ax 'arbitrary
+        let opn_gens = if length op_custom_gens > 0
+                       then delete_i (argi - 1) op_custom_gens
+                       else replicate (argn_op - 1) 'arbitrary
+        let has_constr = opArg_has_constraint opn
+        let op_constr = if has_constr
+                        then varE $ opArg_constraint opn
+                        else [| $(num_args_name opnm >>= constN) True |]
+        let all_gens = ax_gens ++ opn_gens
+        let fargi = flip_n_to_1 argi
+        let app = liftAn argn_ax
+        let app2 = liftA2n (argn_ax + argn_op - 1)
+        let eat_spare_cond_args = eat_args (argn_ax+1) (argn_ax + argn_op - 1)
+        let test_name = gen_label argi opnm axnm
+        [|
+            let lhs = $app ar_lhs $axE
+                rhs = $app ar_rhs $axE
+                app_op_constraint = $app ($fargi $op_constr)
+                lhs_feasible = app_op_constraint lhs
+                rhs_feasible = app_op_constraint rhs
+                op_app = $app ($fargi $opE)
+                op_cond = $app2 both_or_none lhs_feasible rhs_feasible
+                axiom_cond = $eat_spare_cond_args ($app ar_cond $axE)
+            in label test_name $ property $
+                $(apply_gens_to
+                    [| $app2 (==>) axiom_cond $
+                       $app2 (==>) op_cond $
+                       $app2 (==) (op_app lhs) (op_app rhs)
+                    |]
+                    all_gens)
+         |]
+
+both_or_none :: Bool -> Bool -> Bool
+both_or_none a b |      a && b  = True
+both_or_none a b | not (a || b) = False
+both_or_none _ _ | otherwise    = error "Applicability constraint true for only one side of the axiom!"
+
+eat_args :: Int -> Int -> Q Exp
+eat_args from to = [| $(liftAn (from-1)) $(eat_n_args (to-from+1)) |]
+
+eat_n_args :: Int -> ExpQ
+eat_n_args = constN
+
+constN :: Int -> ExpQ
+constN n | n < 0 = fail "argument too small"
+constN 0 = [| id |]
+constN n = [| const . $(constN (n-1)) |]
+
+liftAn :: Int -> ExpQ
+liftAn n | n < 0 = fail "argument too small"
+liftAn 0 = [| id |]
+liftAn n = [| (.) . $(liftAn (n-1)) |]
+
+liftA2n :: Int -> ExpQ
+liftA2n n | n < 0 = fail "argument too small"
+liftA2n 0 = [| id |]
+liftA2n n = [| liftA2 . $(liftA2n (n-1)) |]
+
+flip_n_to_1 :: Int -> ExpQ
+flip_n_to_1 n | n < 1 = fail "argument too small"
+flip_n_to_1 1 = [| id |]
+flip_n_to_1 n = [| flip . (.) $(flip_n_to_1 (n-1)) |]
+
+{- Allows all (i, opn) for which the i'th argument of opn is exactly the type of ax.
+ - It should allow matching types.
+ -}
+filter_ops :: Name -> [(Int, Name)] -> Q [(Int, Name)]
+filter_ops ax = filterM (is_applicable ax)
+
+is_applicable :: Name -> (Int, Name) -> Q Bool
+is_applicable ax (argi, opn) = do xt <- return_type_of_axiom ax
+                                  ot <- type_of_argi argi opn
+                                  return (xt == ot)
+
+filter_Ops :: Axiom -> [OpArg] -> Q [OpArg]
+filter_Ops ax = filterM (is_applicable_Op $ axiom_name ax)
+
+is_applicable_Op :: Name -> OpArg -> Q Bool
+is_applicable_Op ax opn = do xt <- return_type_of_axiom ax
+                             ot <- type_of_argi (opArg_argi opn) (opArg_name opn)
+                             mapM_ warn_if_type_is_polymorphic [xt, ot]
+                             return (xt == ot)
+
+warn_if_type_is_polymorphic :: Type -> Q ()
+warn_if_type_is_polymorphic tp = if type_is_polymorphic tp
+                                 then reportError $ "Polymorphic types are not supported!\n"
+                                                 ++ "Offending type: " ++ pprint tp ++ "\n"
+                                 else return ()
+
+type_is_polymorphic :: Type -> Bool
+type_is_polymorphic tp = case tp of
+    ForallT vars _ tp' -> length vars > 0 || type_is_polymorphic tp'
+    AppT tp' tp'' -> type_is_polymorphic tp' || type_is_polymorphic tp''
+    SigT tp' _ -> type_is_polymorphic tp'
+    VarT _ -> True
+    ConT _ -> False
+    PromotedT _ -> False
+    TupleT _ -> False
+    UnboxedTupleT _ -> False
+    ArrowT -> False
+    ListT -> False
+    PromotedTupleT _ -> False
+    PromotedNilT -> False
+    PromotedConsT -> False
+    StarT -> False
+    ConstraintT -> False
+    LitT _ -> False
+
+{- Axioms return a pair of type (a, a), and we want the type of a.
+ -}
+return_type_of_axiom :: Name -> TypeQ
+return_type_of_axiom name = return_type_of name >>= axiom_result_type
+
+axiom_result_type :: Type -> TypeQ
+axiom_result_type (AppT (ConT nm) tp) | nm == ''AxiomResult = return tp
+axiom_result_type tp = fail $ "Expected ``AxiomResult a'' for some a, but got ``" ++ pprint tp ++ "''"
+
+-- For a type (a, a) returns the type of a.
+pair_type :: Type -> TypeQ
+pair_type (AppT (AppT (TupleT 2) a) b) | a == b = return a
+pair_type tp = fail $ "Expected a pair ``(a, a)'' but got ``" ++ pprint tp ++ "''"
+
+return_type_of :: Name -> TypeQ
+return_type_of = liftM return_type . typeof
+
+type_of_argi :: Int -> Name -> TypeQ
+type_of_argi i = liftM (arg_i_type i) . typeof
+
+return_type :: Type -> Type
+return_type (ForallT _ _ tp) = return_type tp
+return_type (AppT (AppT ArrowT _) tp) = return_type tp
+return_type tp = tp
+
+arg_i_type :: Int -> Type -> Type
+arg_i_type i (ForallT _ _ tp) = arg_i_type i tp
+arg_i_type 1 (AppT (AppT ArrowT tp) _) = tp
+arg_i_type i (AppT (AppT ArrowT _) tp) = arg_i_type (i-1) tp
+arg_i_type i t = error $ "Failed pattern match in arg_i_type.\n"
+    ++ "Please file a bug report and attach the following output.\n"
+    ++ "i=" ++ show i ++ "\n"
+    ++ show t
diff --git a/Test/OITestGenerator/Axiom.hs b/Test/OITestGenerator/Axiom.hs
new file mode 100644
--- /dev/null
+++ b/Test/OITestGenerator/Axiom.hs
@@ -0,0 +1,92 @@
+{-# LANGUAGE TemplateHaskell #-}
+
+-- | This file should not be imported directly. Import "Test.OITestGenerator"
+--   instead.
+module Test.OITestGenerator.Axiom (
+    Axiom(),
+    axiom, withGens, axiom_name, axiom_gens,
+    AxiomResult(),
+    ar_cond, ar_lhs, ar_rhs, (=!=), (===>)
+) where
+
+import Data.Label
+import Language.Haskell.TH
+import Prelude
+import Test.OITestGenerator.GenHelper
+import Test.OITestGenerator.HasGens
+
+newtype AxiomResult a = AxiomResult (Bool, a, a)
+
+infix 1 =!=
+-- | Combine the results of the left- and right-hand sides of an axiom.
+--   A simple example is
+--
+--   > q1 :: AxiomResult Bool
+--   > q1 = isEmpty empty =!= True
+--
+--   while an axiom with variables would be written as a function like this:
+--
+--   > q2 :: Int -> IntQueue -> AxiomResult Bool
+--   > q2 x q = isEmpty (enqueue x q) =!= False
+(=!=) :: a -> a -> AxiomResult a
+lhs =!= rhs = AxiomResult (True, lhs, rhs)
+
+infixr 0 ===>
+-- | Adds a condition to an axiom. If the 'Bool' argument is 'False', the axiom
+--   won't be evaluated. The test will neither count as a failed test, nor as
+--   a successful test. It translates to QuickChecks '==>' operator.
+--
+--   Example usage:
+--
+-- > q4 :: Int -> IntQueue -> AxiomResult Int
+-- > q4 x q = not (isEmpty q) ===> front (enqueue x q) =!= front q
+(===>) :: Bool -> AxiomResult a -> AxiomResult a
+cond ===> AxiomResult (cond', lhs, rhs) = AxiomResult (cond && cond', lhs, rhs)
+
+ar_cond :: AxiomResult a -> Bool
+ar_cond (AxiomResult (cond, _, _)) = cond
+
+ar_lhs :: AxiomResult a -> a
+ar_lhs (AxiomResult (_, lhs, _)) = lhs
+
+ar_rhs :: AxiomResult a -> a
+ar_rhs (AxiomResult (_, _, rhs)) = rhs
+
+data Axiom = Axiom {
+    _name :: Name,
+    _gens :: Q [Name]
+}
+
+mkLabel ''Axiom
+
+-- | 'Axiom' constructor. Takes a 'Language.Haskell.TH.Syntax.Name', i.e.
+--
+-- > axiom 'q1
+--
+-- or
+--
+-- > map axiom ['q1, 'q2, 'q3]
+--
+-- .
+axiom :: Name -> Axiom
+axiom name' = Axiom {
+    _name = name',
+    _gens = return []
+}
+
+axiom_name :: Axiom -> Name
+axiom_name = get name
+
+axiom_gens :: Axiom -> Q [Name]
+axiom_gens = get gens
+
+instance HasGens Axiom where
+    withGens axiom' gens' = flip (set gens) axiom' $
+                            let qargn = num_args_name nm
+                                nm = get name axiom'
+                            in qargn >>= \argn ->
+                               if argn == length gens'
+                               then return gens'
+                               else fail $ "Axiom " ++ show nm ++ " has "
+                                    ++ show argn ++ " arguments, but "
+                                    ++ show (length gens') ++ " Gens are given"
diff --git a/Test/OITestGenerator/GenHelper.hs b/Test/OITestGenerator/GenHelper.hs
new file mode 100644
--- /dev/null
+++ b/Test/OITestGenerator/GenHelper.hs
@@ -0,0 +1,30 @@
+-- | This file should not be imported directly. Import "Test.OITestGenerator"
+--   instead.
+module Test.OITestGenerator.GenHelper (
+    num_args_name, num_args, typeof
+) where
+
+import Prelude
+import Language.Haskell.TH
+import Control.Applicative
+import Control.Monad
+
+num_args_name :: Name -> Q Int
+num_args_name name = liftM num_args $ typeof name
+
+num_args :: Type -> Int
+num_args (ForallT _ _ tp) = num_args tp
+num_args (AppT (AppT ArrowT _) tp) = 1 + num_args tp
+num_args _ = 0
+
+typeof_info :: Info -> Type
+typeof_info (VarI _ tp _ _)      = tp
+typeof_info (ClassOpI _ tp _ _)  = tp
+typeof_info (DataConI _ tp _ _)  = tp
+typeof_info (TyVarI _ tp)        = tp
+typeof_info t = error $ "Failed pattern match in typeof_info.\n"
+    ++ "Please file a bug report and attach the following output.\n"
+    ++ show t
+
+typeof :: Name -> TypeQ
+typeof name = liftM typeof_info $ reify name
diff --git a/Test/OITestGenerator/HasGens.hs b/Test/OITestGenerator/HasGens.hs
new file mode 100644
--- /dev/null
+++ b/Test/OITestGenerator/HasGens.hs
@@ -0,0 +1,15 @@
+-- | This file should not be imported directly. Import "Test.OITestGenerator"
+--   instead.
+module Test.OITestGenerator.HasGens (
+    HasGens(..)
+) where
+
+import Language.Haskell.TH
+import Prelude
+
+class HasGens a where
+    -- | Use to specify custom generators for the given operation or axiom. The
+    -- @i@-th element of the list corresponds to the @i@-th argument. All
+    -- generators must be specified. Not using a custom generator for specific
+    -- arguments can be achieved by passing 'arbitrary'.
+    withGens :: a -> [Name] -> a
diff --git a/Test/OITestGenerator/Op.hs b/Test/OITestGenerator/Op.hs
new file mode 100644
--- /dev/null
+++ b/Test/OITestGenerator/Op.hs
@@ -0,0 +1,100 @@
+{-# LANGUAGE TemplateHaskell #-}
+
+-- | This file should not be imported directly. Import "Test.OITestGenerator"
+--   instead.
+module Test.OITestGenerator.Op (
+    Arg(), Op(),
+    op, arg,
+    but, only, withGens, withConstraint,
+    op_name, op_args, op_gens, op_has_constraint, op_constraint, op_maybe_constraint
+) where
+
+import Control.Monad
+import Data.Label
+import Data.List
+import Data.Maybe
+import Language.Haskell.TH
+import Prelude
+import Test.OITestGenerator.GenHelper
+import Test.OITestGenerator.HasGens
+
+-- | An operation. Contains information about the operation's name, which
+-- arguments may be tested (all by default), which generators should be used for
+-- each argument ('arbitrary' by default) and possibly a constraint function.
+data Op = Op {
+    _name :: Name,
+    _argis :: Q [Int],
+    _gens :: Q [Name],
+    _constraint :: Maybe Name
+}
+
+mkLabel ''Op
+
+type Arg = Int
+
+-- | 'Arg' constructor. Only for readability.
+arg :: Int -> Arg
+arg = id
+
+-- | 'Op' constructor.
+op :: Name -> Op
+op name' = Op {
+    _name = name',
+    _argis = liftM (enumFromTo 1) $ num_args_name name',
+    _gens = return [],
+    _constraint = Nothing
+}
+
+-- | @but o i@ excludes the @i@-th argument from @o@ when generating tests.
+--
+-- Example:
+--
+-- > op 'dequeue `but` arg 1
+but :: Op -> Arg -> Op
+but op' excl = modify argis (liftM $ delete excl) op'
+
+-- | @only o i@ excludes all but the @i@-th argument from @o@ when generating tests.
+--
+-- Example:
+--
+-- > op 'dequeue `only` arg 1
+only :: Op -> Arg -> Op
+only op' argi = modify argis (>>= \args ->
+        if argi `elem` args
+        then return [argi]
+        else fail $ "Argument #" ++ show argi ++ " is not in " ++ show args
+    ) op'
+
+instance HasGens Op where
+    op' `withGens` gens' = flip (set gens) op' $
+                            let qargn = num_args_name nm
+                                nm = get name op'
+                            in qargn >>= \argn ->
+                               if argn == length gens'
+                               then return gens'
+                               else fail $ "Operator " ++ show nm ++ " has "
+                                   ++ show argn ++ " arguments, but "
+                                   ++ show (length gens') ++ " Gens are given"
+
+-- | @op `withConstraint` f@ adds a constraint function @f@ to @op@. @f@ must
+-- take arguments of the same type as @op@ and return a 'Bool'. 
+withConstraint :: Op -> Name -> Op
+op' `withConstraint` constraint' = set constraint (Just constraint') op'
+
+op_name :: Op -> Name
+op_name = get name
+
+op_args :: Op -> Q [Int]
+op_args = get argis
+
+op_gens :: Op -> Q [Name]
+op_gens = get gens
+
+op_has_constraint :: Op -> Bool
+op_has_constraint = isJust . get constraint
+
+op_constraint :: Op -> Name
+op_constraint = fromJust . get constraint
+
+op_maybe_constraint :: Op -> Maybe Name
+op_maybe_constraint = get constraint
diff --git a/Test/OITestGenerator/OpArg.hs b/Test/OITestGenerator/OpArg.hs
new file mode 100644
--- /dev/null
+++ b/Test/OITestGenerator/OpArg.hs
@@ -0,0 +1,55 @@
+{-# LANGUAGE TemplateHaskell #-}
+
+-- | This file should not be imported directly. Import "Test.OITestGenerator"
+--   instead.
+module Test.OITestGenerator.OpArg (
+    OpArg(), opArg,
+    opArg_name, opArg_argi, opArg_gens, opArg_has_constraint, opArg_constraint,
+    op2opArgs
+) where
+
+import Data.Label
+import Data.Maybe
+import Language.Haskell.TH
+import Prelude
+import Test.OITestGenerator.Op
+
+data OpArg = OpArg {
+    _name :: Name,
+    _argi :: Int,
+    _gens :: [Name],
+    _constraint :: Maybe Name
+}
+
+mkLabel ''OpArg
+
+opArg :: Name -> Int -> [Name] -> Maybe Name -> OpArg
+opArg name' argi' gens' constraint' = OpArg {
+    _name = name',
+    _argi = argi',
+    _gens = gens',
+    _constraint = constraint'
+}
+
+op2opArg :: Op -> Int -> Q OpArg
+op2opArg opn argi' = do
+    gens' <- op_gens opn
+    return $ opArg (op_name opn) argi' gens' (op_maybe_constraint opn)
+
+op2opArgs :: Op -> Q [OpArg]
+op2opArgs opn = op_args opn >>= mapM (op2opArg opn)
+
+opArg_name :: OpArg -> Name
+opArg_name = get name
+
+opArg_argi :: OpArg -> Int
+opArg_argi = get argi
+
+opArg_gens :: OpArg -> [Name]
+opArg_gens = get gens
+
+opArg_has_constraint :: OpArg -> Bool
+opArg_has_constraint = isJust . get constraint
+
+opArg_constraint :: OpArg -> Name
+opArg_constraint = fromJust . get constraint
diff --git a/qc-oi-testgenerator.cabal b/qc-oi-testgenerator.cabal
new file mode 100644
--- /dev/null
+++ b/qc-oi-testgenerator.cabal
@@ -0,0 +1,26 @@
+-- Initial qc-oi-testgenerator.cabal generated by cabal init.  For further 
+-- documentation, see http://haskell.org/cabal/users-guide/
+
+name:                qc-oi-testgenerator
+version:             1.2.0.1
+synopsis:            Compile time generation of operation invariance tests for QuickCheck
+-- description:
+--homepage:            http://tobias.goedderz.info/haskell/qc-oi-testgenerator/
+homepage:            http://www.iai.uni-bonn.de/~jv/GV14.html
+license:             BSD3
+license-file:        LICENSE
+author:              Tobias Gödderz
+maintainer:          haskell@tobias.goedderz.info
+-- copyright:
+category:            Testing
+build-type:          Simple
+-- extra-source-files:
+cabal-version:       >=1.10
+
+library
+  exposed-modules:     Test.OITestGenerator, Test.OITestGenerator.HasGens, Test.OITestGenerator.OpArg, Test.OITestGenerator.Op, Test.OITestGenerator.GenHelper, Test.OITestGenerator.Axiom
+  -- other-modules:
+  other-extensions:    TemplateHaskell
+  build-depends:       base >=4.6 && <4.7, template-haskell >=2.8 && <2.9, QuickCheck >=2.6 && <2.8, fclabels >=2.0 && <2.1
+  -- hs-source-dirs:
+  default-language:    Haskell2010