{-# 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"