module PropLogicTest (

  -- * Convenient abbreviations and combinations of often used functions

  -- ** Various prime form generations
  pdnf', pcnf',
  spdnf', spcnf',
  xpdnf', xpcnf',

  -- ** Various prime form generations with combined parsing and display
  pdnf, pcnf,
  spdnf, spcnf,
  xpdnf, xpcnf,

  -- * Random generation

  -- ** Auxiliary random functions (probably obsolete)

  randomListMember,
  -- | For example,
  --
  -- > > randomListMember ['a','b','c','d']
  -- > 'b'
  -- > > randomListMember ['a','b','c','d']
  -- > 'd'
  -- > > randomListMember ['a','b','c','d']
  -- > 'c'

  randomChoice,
  -- | Removes one random member from a given list and returns this member and the remaining list. For example,
  --
  -- > > randomChoice ["a", "b", "c"]
  -- > ("c",["a","b"])
  -- > > randomChoice ["a", "b", "c"]
  -- > ("b",["a","c"])
  -- > > randomChoice ["a", "b", "c"]
  -- > ("a",["b","c"])
  -- > > randomChoice ["a", "b", "c"]
  -- > ("a",["b","c"])

  shuffle,
  -- | For example,
  --
  -- > > shuffle [1,2,3,2,1]
  -- > [2,1,3,1,2]
  -- > > shuffle [1,2,3,2,1]
  -- > [1,2,3,2,1]
  -- > > shuffle [1,2,3,2,1]
  -- > [2,1,2,3,1]
  -- > > shuffle [1,2,3,2,1]
  -- > [2,3,1,1,2]
  -- > > shuffle [1,2,3,2,1]
  -- > [2,1,1,3,2]
  -- > > shuffle [1,2,3,2,1]
  -- > [1,2,1,3,2]

  randomSublist,
  -- | @randomSublist xL@ deletes a random number of members and returns the result. For example,
  --
  -- > > randomSublist [1,2,3,4,5,6,7,7,7,8,8,8]
  -- > [4]
  -- > > randomSublist [1,2,3,4,5,6,7,7,7,8,8,8]
  -- > [3,4]
  -- > > randomSublist [1,2,3,4,5,6,7,7,7,8,8,8]
  -- > [2,3,4,5,6,7,7,7,8,8]
  -- > > randomSublist [1,2,3,4,5,6,7,7,7,8,8,8]
  -- > [1,2,5,7,8]
  -- > > randomSublist [1,2,3,4,5,6,7,7,7,8,8,8]
  -- > [4,5,8,8]
  -- > > randomSublist [1,2,3,4,5,6,7,7,7,8,8,8]
  -- > [1,2,3,5,6,7,7,8,8]

  nRandomRIO,
  -- | @nRandomRIO n (lower,upper)@ returns an list of n random integers between lower and upper.
  -- For example,
  --
  -- > > nRandomRIO 10 (1,3)
  -- > [2,3,3,2,2,3,3,3,3,1]
  -- > > nRandomRIO 10 (1,3)
  -- > [3,2,1,2,2,3,3,1,1,1]
  -- > > nRandomRIO 10 (1,3)
  -- > [1,3,2,1,2,1,2,2,1,2]

  weightedRandomMember,
  -- | @weightedRandomMember@ takes a list @[(x1,n1),...,(xM,nM)]@ of @(a,Int)@ pairs and selects one of the @x1,...,xM@.
  -- The second integer value @ni@ in each pair @(xi,ni)@ represents the relative likelihood for the choice of @xi@ compare to the
  -- other values. In the following example and on the long run, @a@ is chosen 10 times more often than @b@, and @c@ isn't chosen at all.
  --
  -- > > weightedRandomMember [("a",10),("b",1),("c",0)]
  -- > "a"
  -- > > weightedRandomMember [("a",10),("b",1),("c",0)]
  -- > "a"
  -- > > weightedRandomMember [("a",10),("b",1),("c",0)]
  -- > "a"
  -- > > weightedRandomMember [("a",10),("b",1),("c",0)]
  -- > "a"
  -- > > weightedRandomMember [("a",10),("b",1),("c",0)]
  -- > "a"
  -- > > weightedRandomMember [("a",10),("b",1),("c",0)]
  -- > "a"
  -- > > weightedRandomMember [("a",10),("b",1),("c",0)]
  -- > "a"
  -- > > weightedRandomMember [("a",10),("b",1),("c",0)]
  -- > "b"
  -- > > weightedRandomMember [("a",10),("b",1),("c",0)]
  -- > "a"

  appleBasketDistribution,
  -- | @appleBasketDistribution n k@ distributes @n@ apples into @k@ baskets in the sense that the result is a random integer list
  -- of length @k@, where the sum of its components is @n@.
  --
  -- > > appleBasketDistribution 10 4
  -- > [4,2,2,2]
  -- > > appleBasketDistribution 10 4
  -- > [2,2,3,3]
  -- > > appleBasketDistribution 10 4
  -- > [3,2,1,4]
  -- > > appleBasketDistribution 10 4
  -- > [0,7,0,3]

  -- ** Random I-Forms and X-Forms

  averageLineLength,
  randomILine,
  randomIForm,
  randomXForm,

  -- ** Random DNFs and CNFs

  randomDNF,
  randomCNF,
  randomCharDNF, randomCharCNF,
  randomIntDNF, randomIntCNF,

  -- ** Random propositional formulas in general

  -- *** Size parameter

  SizeTriple,

  sizeTriple,

  -- *** Random formulas

  JunctorSymbol(..),

  JunctorWeighting,

  defaultJunctorWeighting,

  weightedRandomPropForm,

  randomPropForm,
  -- | @randomPropForm aL (aSize,jSize)@ returns a randomly generated propositional formula @p@ such that
  --
  -- >     atoms p    == aL
  -- >     atomSize p == aSize
  -- >     juncSize p == jSize
  --
  -- If @atomSize@ is smaller than the length of @aL@, an error message is returned. For example,
  --
  -- > > randomPropForm ["x", "y"] (3,3)
  -- > EJ [A "y",T,A "y",A "x",DJ []]
  -- > > randomPropForm ["x", "y"] (3,3)
  -- > EJ [SJ [A "y",A "y"],DJ [A "x"]]
  -- > > randomPropForm ["x", "y"] (3,3)
  -- > EJ [EJ [],A "x",CJ [A "y"],A "x"]
  -- > > randomPropForm ['x','y','z'] (1,1)
  -- > *** Exception: randomPropForm -- atom size smaller than ordered atom list

  randomCharProp,
  -- | @randomCharProp (aCard,aSize,jSize)@ is @randomPropForm aL (aSize,jSize)@, where @aL@ is the ordered list of the first @aCard@
  -- small characters @'a', 'b', 'c', ...@. If the atom cardinality is undefined, i.e. if not @0<=aCard<=26@, or if it exceeds @aSize@,
  -- an error message is returned.
  -- For example,
  --
  -- > > randomCharProp (3,5,5)
  -- > SJ [A 'c',EJ [A 'a',A 'c'],F,T,DJ [A 'b'],A 'c']
  -- > > randomCharProp (3,5,5)
  -- > SJ [A 'a',A 'c',DJ [T,CJ [A 'b',A 'a',A 'b'],T]]
  -- > > randomCharProp (3,5,5)
  -- > DJ [F,A 'b',SJ [F],A 'c',DJ [A 'a'],A 'c',A 'a']

  randomIntProp,

  -- * Testing

  -- ** Testing a propositional algebra

  -- *** Axioms of propositional algebras
  axiom_reflexivity_of_subvalence,
  axiom_transitivity_of_subvalence,
  axiom_criterion_for_equivalence,
  -- | CONTINUEHERE ..............................................................!!

  -- *** The summarized test function for a propositional algebra
  test_prop_alg,

  -- ** Tests for "DefaultPropLogic"

  -- *** Testing the normalizations

  -- | ...continuehere...............................

  -- *** Testing the default propositional algebras

  -- ** Tests for "FastPropLogic"

  -- *** Testing of the M- and P-procedure
  -- | continuehere ............................

  -- *** Correctness of the Prime Normal Form constructions
  -- | continuehere ...........................

  -- ** Test for the total package
  total_test,

  -- * Profiling - first version

  -- ** Measures

  Msec,
  CanonPerformance,
  Verbose,

  -- ** correctness tests (move these correctness tests)--!!!!!!!!!!1

  pnfCorrect,
  pnfCorrectRepeat,

  -- ** performance tests

  pnfPerform,
  pnfPerformRandom,
  pnfPerformRepeat,

  -- * Profiling - second version
  Seconds,
  verboseRandomPrimeTest,
  verboseRandomPrimeTesting,
  meanValue,
  standDeviation,
  normSeconds,

) where ---------------------------------------------------------------------------------------------------------------

  import Data.Char (chr)
  import Data.Ratio
  import System.Random (randomIO, randomRIO)
  import Control.Monad
  import System.CPUTime (getCPUTime)
  import qualified System.Time  as T
  import qualified Olist as O
  import qualified TextDisplay as D
  import qualified Costack as C
  import PropLogicCore
  import DefaultPropLogic
  import FastPropLogic

-- convenient abbreviations

  pdnf' :: Ord a => PropForm a -> PDNF a
  pdnf' = fromXPDNF . toXPDNF

  pcnf' :: Ord a => PropForm a -> PCNF a
  pcnf' = fromXPCNF . toXPCNF

  spdnf' :: Ord a => PropForm a -> SimpleDNF a
  spdnf' = simpleDNF . pdnf'

  spcnf' :: Ord a => PropForm a -> SimpleCNF a
  spcnf' = simpleCNF . pcnf'

  xpdnf' :: Ord a => PropForm a -> XPDNF a               -- this should go to the FastPropLogic module!!!!!!!!!!!!!!!!
  xpdnf' = toXPDNF

  xpcnf' :: Ord a => PropForm a -> XPCNF a               -- this should go to the FastPropLogic module!!!!!!!!!!!!!!!!
  xpcnf' = toXPCNF

  pdnf :: String -> IO ()
  pdnf = D.display . pdnf' . stringToProp

  pcnf :: String -> IO ()
  pcnf = D.display . pcnf' . stringToProp

  spdnf :: String -> IO ()
  spdnf = D.display . spdnf' . stringToProp

  spcnf :: String -> IO ()
  spcnf = D.display . spcnf' . stringToProp

  xpdnf :: String -> IO ()
  xpdnf = D.display . xpdnf' . stringToProp

  xpcnf :: String -> IO ()
  xpcnf = D.display . xpcnf' . stringToProp

-- auxiliary random functions

  randomListMember :: [a] -> IO a
  randomListMember xL = do i <- randomRIO (0, length xL - 1)
                           return (xL !! i)

  randomChoice :: [a] -> IO (a, [a])
  randomChoice [] = error "randomChoice -- empty list"
  randomChoice xL = do i <- randomRIO (0, length xL -1)
                       let (yL, z:zL) = splitAt i xL
                       return (z, yL ++ zL)

  nRandomListMember :: Int -> [a] -> IO [a]
  nRandomListMember n xL = mapM randomListMember (replicate n xL)

  randomInsert :: a -> [a] -> IO [a]
  randomInsert x xL = do i <- randomRIO (0, length xL)
                         let (yL,zL) = splitAt i xL
                         return (yL ++ [x] ++ zL)

  shuffle :: [a] -> IO [a]
  shuffle xL = if null xL
               then return []
               else do (y,yL) <- randomChoice xL
                       zL <- shuffle yL
                       return (y:zL)

  randomSublist :: [a] -> IO [a]
  randomSublist xL = do let n = length xL -1
                        k <- randomRIO (0, n)
                        iL <- shuffle [1..n]
                        let jL = O.olist (take k iL)
                        let yL = filtering xL jL 1
                        return yL
    where filtering xL [] _ = []
          filtering (x:xL) (j:jL) i = if j == i
                                      then x : (filtering xL jL (i + 1))
                                      else filtering xL (j:jL) (i + 1)

  nRandomRIO :: Int -> (Int,Int) -> IO [Int]
  nRandomRIO n (lower,upper) = sequence (replicate n (randomRIO (lower,upper)))

  weightedRandomMember :: [(a,Int)] -> IO a
  weightedRandomMember pairL = do i <- randomRIO (1, sum (map snd pairL))
                                  return (select pairL i)
    where select ((x,k):pL) i = if i <= k
                                then x
                                else select pL (i - k)

  appleBasketDistribution :: Int -> Int -> IO [Int]
  appleBasketDistribution apples baskets =
    if apples < 0 || baskets < 0
    then error "appleBasketDistribution -- negative arguments"
    else if baskets == 0
         then if apples == 0
              then return []
              else error "appleBasketDistribution -- zero baskets"
         else do basketIndexList <- nRandomRIO apples (0, baskets - 1)
                 return (map (\ i -> count i basketIndexList) (Prelude.take baskets (enumFrom 0)))
    where count x yL = length (filter (\ y -> y == x) yL)

-- random I-Forms and X-Forms

  averageLineLength :: IForm -> Float
  averageLineLength iform = (fromIntegral (truncate ((v / l) * 100))) / 100
    where v = fromIntegral (volume iform) :: Float
          l = fromIntegral (C.length iform) :: Float

  randomILine :: Int -> Int -> IO ILine
  randomILine atomNum averLen =
    do intLL <- mapM singleAtom [1..atomNum]
       let intL = concat intLL
       return (iLine intL)
    where singleAtom :: IAtom -> IO [ILit]
          singleAtom atom = do i <- randomRIO (1, atomNum)
                               b <- randomIO :: IO Bool
                               let lit = if i <= averLen
                                         then if b then [atom] else [negLit atom]
                                         else []
                               return lit

  randomIForm :: Int -> Int -> Int -> IO IForm

--  randomIForm atomNum formLen averLineLen =
--    do lineL <- sequence (replicate formLen (randomILine atomNum averLineLen))
--       return (C.fromList lineL)

  randomIForm atomNum formLen averLineLen
    | atomNum < 0 = error "randomIForm -- negative number of atoms"
    | formLen < 0 = error "randomIForm -- negative I-Form length"
    | averLineLen < 0 = error "randomIForm -- negative average I-Line length"
    | atomNum < averLineLen = error "randomIForm -- atom number smaller than average I-Line length"
    | otherwise   =  do lineL <- sequence (replicate formLen (randomILine atomNum averLineLen))
                        return (C.fromList lineL)

  randomXForm :: Ord a => [a] -> Int -> Int -> IO (XForm a)
  randomXForm atomL formLen averLineLen =
    do let ordAtomL = O.olist atomL
       let atomNum = length ordAtomL
       iform <- randomIForm atomNum formLen averLineLen
       return (ordAtomL, iform)

-- random DNFs and CNFs

  randomDNF :: Ord a => [a] -> Int -> Int -> IO (DNF a)
  randomDNF atomL formLen averLineLen = do xform <- randomXForm atomL formLen averLineLen
                                           return (xDNF xform)

  randomCNF :: Ord a => [a] -> Int -> Int -> IO (CNF a)
  randomCNF atomL formLen averLineLen = do xform <- randomXForm atomL formLen averLineLen
                                           return (xCNF xform)

  randomCharDNF :: Int -> IO (DNF Char)
  randomCharDNF atomNum = randomDNF (take atomNum ['a'..'z']) (2 * atomNum) atomNum

  randomCharCNF :: Int -> IO (CNF Char)
  randomCharCNF atomNum = randomCNF (take atomNum ['a'..'z']) (2 * atomNum) atomNum

  randomIntDNF :: Int -> IO (DNF Int)
  randomIntDNF atomNum = randomDNF (take atomNum [1..]) (2 * atomNum) atomNum

  randomIntCNF :: Int -> IO (CNF Int)
  randomIntCNF atomNum = randomCNF (take atomNum [1..]) (2 * atomNum) atomNum

-- size parameters

  type SizeTriple = (Int,Int,Int) -- = (length atoms, atomSize, juncSize)

  sizeTriple :: Ord a => PropForm a -> SizeTriple
  sizeTriple p = (Prelude.length (atoms p), atomSize p, juncSize p)

-- random formula generation with weighted junctors

  data JunctorSymbol = T_ | F_ | N_ | CJ_ | DJ_ | SJ_ | EJ_
    deriving (Eq, Ord, Show, Read)

  type JunctorWeighting = [(JunctorSymbol, Int)]

  defaultJunctorWeighting :: JunctorWeighting
  defaultJunctorWeighting = [(N_,15), (F_,1), (T_,1), (CJ_,5), (DJ_,5), (SJ_,1), (EJ_,1)]

  weightedRandomPropForm :: JunctorWeighting -> O.Olist a -> (Int, Int) -> IO (PropForm a)
  weightedRandomPropForm weighting ordAtomL (aSize,jSize)
    | aSize < 0 || jSize < 0            = error "weightedRandomPropForm -- negative size"
    | aSize == 0 && jSize == 0          = error "weightedRandomPropForm -- zero atom and junctor size"
    | aSize > 0 && length ordAtomL == 0 = error "weightedRandomPropForm -- no atoms available"
    | aSize < length ordAtomL           = error "weightedRandomPropForm -- atom size smaller than ordered atom list"
    | otherwise = do aL <- nRandomListMember (aSize - (length ordAtomL)) ordAtomL
                     aL <- shuffle (aL ++ ordAtomL)
                     p <- iter jSize (map A aL)
                     return p
    where iter :: Int -> [PropForm a] -> IO (PropForm a)
          iter jSize pL | jSize == 0 = if length pL == 1
                                       then return (head pL)
                                       else error "weightedRandomPropForm -- junctor size"
                        | jSize == 1 = do x <- if length pL == 0
                                               then randomJunc [CJ_, DJ_, SJ_, EJ_, F_, T_]
                                               else randomJunc [CJ_, DJ_, SJ_, EJ_]
                                          p <- case x of
                                                  F_  -> return F
                                                  T_  -> return T
                                                  CJ_ -> return (CJ pL)
                                                  DJ_ -> return (DJ pL)
                                                  SJ_ -> return (SJ pL)
                                                  EJ_ -> return (EJ pL)
                                          return p
                        | jSize >= 2 = do x <- if length pL == 0
                                               then randomJunc [F_, T_, CJ_, DJ_, SJ_, EJ_]
                                               else randomJunc [F_, T_, CJ_, DJ_, SJ_, EJ_, N_]
                                          qL <- case x of
                                                  F_ -> do let pL' = F : pL
                                                           pL'' <- shuffle pL'
                                                           return pL'
                                                  T_ -> do let pL' = T : pL
                                                           pL'' <- shuffle pL'
                                                           return pL'
                                                  N_ -> do (p',pL') <- randomChoice pL
                                                           pL'' <- shuffle ((N p') : pL')
                                                           return pL''
                                                  _  -> do i <- randomRIO (0, length pL - 1)
                                                           let (pL1, pL2) = splitAt i pL
                                                           let q = case x of
                                                                     CJ_ -> (CJ pL1)
                                                                     DJ_ -> (DJ pL1)
                                                                     SJ_ -> (SJ pL1)
                                                                     EJ_ -> (EJ pL1)
                                                           pL' <- shuffle (q : pL2)
                                                           return pL'
                                          p <- iter (jSize - 1) qL
                                          return p
          randomJunc :: [JunctorSymbol] -> IO JunctorSymbol
          randomJunc selection = weightedRandomMember (select selection weighting)
             where select [] _ = []
                   select (x:xL) pL = (select1 x pL) : (select xL pL)
                   select1 x ((y,n):pL) = if x == y
                                          then (y,n)
                                          else select1 x pL

  randomPropForm :: O.Olist a -> (Int,Int) -> IO (PropForm a)
  randomPropForm ordAtomL (aSize,jSize)
    | aSize < 0 || jSize < 0            = error "randomPropForm -- negative size"
    | aSize == 0 && jSize == 0          = error "randomPropForm -- zero atom and junctor size"
    | aSize > 0 && length ordAtomL == 0 = error "randomPropForm -- no atoms available"
    | aSize < length ordAtomL           = error "randomPropForm -- atom size smaller than ordered atom list"
    | otherwise = do aL <- nRandomListMember (aSize - (length ordAtomL)) ordAtomL
                     aL <- shuffle (aL ++ ordAtomL)
                     p  <- weightedRandomPropForm defaultJunctorWeighting aL (aSize,jSize)
                     return p

  randomCharProp :: SizeTriple -> IO (PropForm Char)
  randomCharProp (aCard,aSize,jSize) =
    if aCard < 0 || aCard > 26
    then error ("randomCharProp -- " ++ (show aCard) ++ " exceeds the number of available 26 characters")
    else do let aL = take aCard charList
            p <- randomPropForm aL (aSize,jSize)
            return p
    where charList = map chr [97..122] -- all small characters 'a', ..., 'z'

  randomIntProp :: SizeTriple -> IO (PropForm Int)
  randomIntProp (aCard,aSize,jSize) = do let aL = Prelude.take aCard [1..]
                                         p <- randomPropForm aL (aSize,jSize)
                                         return p

-- axioms of propositional algebras

  -- the conversion axioms

{--
  axiom_atom_conversion :: PropAlg a p => a -> Bool
  axiom_atom_conversion a = undefined

  -- ambiguous constraint error: -----!!!!!!!!!!!!!
  -- axiom_zero_conversion :: PropAlg a p => Bool
  -- axiom_zero_conversion = fromPropForm F `biequivalent` false

  -- ambiguous constraint error: -----!!!!!!!!!!!!!
  -- axiom_unit_conversion :: PropAlg a p => Bool
  -- axiom_unit_conversion = fromPropForm T `biequivalent` true

  axiom_neg_conversion :: PropAlg a p => PropForm a -> Bool
  axiom_neg_conversion p = fromPropForm (N p) `biequivalent` neg (fromPropForm p)

  ...............etc......................
-}

  -- semantic axioms

  axiom_reflexivity_of_subvalence :: PropAlg a p => p -> Bool
  axiom_reflexivity_of_subvalence p = p `subvalent` p

  axiom_transitivity_of_subvalence :: PropAlg a p => (p,p,p) -> Bool
  axiom_transitivity_of_subvalence (p1,p2,p3) = ((p1 `subvalent` p2) && (p2 `subvalent` p3)) `subvalent` (p1 `subvalent` p3)

  axiom_criterion_for_equivalence :: PropAlg a p => (p,p) -> Bool
  axiom_criterion_for_equivalence (p1,p2) = (p1 `equivalent` p2) `equivalent` ((p1 `subvalent` p2) && (p2 `subvalent` p1))

  axiom_least_element :: PropAlg a p => p -> Bool
  axiom_least_element p = false `subvalent` p

  axiom_greatest_element :: PropAlg a p => p -> Bool
  axiom_greatest_element p = p `subvalent` true

  axiom_neutral_disjunction_element :: PropAlg a p => p -> Bool
  axiom_neutral_disjunction_element p = disj [false, p] `equivalent` p

  axiom_neutral_conjunction_element :: PropAlg a p => p -> Bool
  axiom_neutral_conjunction_element p = conj [true, p] `equivalent` p

  axiom_conjunctive_complement :: PropAlg a p => p -> Bool
  axiom_conjunctive_complement p = conj [p, neg p] `equivalent` false

  axiom_disjunctive_complement :: PropAlg a p => p -> Bool
  axiom_disjunctive_complement p = disj [p, neg p] `equivalent` true

  axiom_conjunctive_idempotency :: PropAlg a p => p -> Bool
  axiom_conjunctive_idempotency p = conj [p, p] `equivalent` p

  axiom_disjunctive_idempotency :: PropAlg a p => p -> Bool
  axiom_disjunctive_idempotency p = disj [p, p] `equivalent` p

  -- CONTINUEHERE ----------------!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!

-- test functions for propositional algebras

  test_prop_alg :: (Show a, Show p, PropAlg a p) => IO a -> IO p -> Int -> IO ()
  test_prop_alg randAtom randProp number =
    do -- generation of random arguments
       atomL <- replicateM number randAtom
       propL <- replicateM number randProp
       propL' <- replicateM number randProp
       propL'' <- replicateM number randProp
       let propPairL = zip propL propL'
       let propTripleL = zip3 propL propL' propL''
       -- test the single axioms
       test_axiom "reflexivity of the subvalence relation"  axiom_reflexivity_of_subvalence propL
       test_axiom "transitivity of the subvalence relation" axiom_transitivity_of_subvalence propTripleL
       test_axiom "criterion for equivalence"               axiom_criterion_for_equivalence propPairL
       -- CONTINUEHERE ...........................
       -- finish
       print "Test for propositional algebra finished successfully."
    where test_axiom :: Show a => String -> (a -> Bool) -> [a] -> IO ()
          test_axiom name axiom [] = print ("test for " ++ name ++ " passed " ++ show number ++ " times")
          test_axiom name axiom (arg:argL) = if axiom arg
                                             then test_axiom name axiom argL
                                             else error (name ++ " doesn't hold for " ++ "\n" ++ show arg)

-- test for the total package

  total_test :: Int -> IO ()
  total_test = undefined

-- measures and test parameters

  type Msec = Integer -- milliseconds

  timeDiffToMsec :: T.TimeDiff -> Msec
  timeDiffToMsec td =
    if T.tdMonth td /= 0 || T.tdYear td /= 0
    then error "timeDiffToMsec -- cannot deal with non-zero months or years"
    else (div (T.tdPicosec td) 1000000000) +
         (toInteger (T.tdSec td)  * 1000) +
         (toInteger (T.tdMin td)  * 1000 * 60) +
         (toInteger (T.tdHour td) * 1000 * 60 * 60) +
         (toInteger (T.tdDay td)  * 1000 * 60 * 60 * 24)

  diffTimes :: T.ClockTime -> T.ClockTime -> Msec
  diffTimes t1 t2 = timeDiffToMsec (T.diffClockTimes t1 t2)

  type CanonPerformance = (SizeTriple,(Msec,SizeTriple),(Msec,SizeTriple)) -- (pre-size, (D-time, D-size), (C-time, C-size))

  type Verbose = Bool  -- set True means that the according function produces additional information while in progress

-- correctness tests

  pnfCorrect :: (D.Display a, Show a, Ord a) => Verbose -> PropForm a -> IO (Either (PropForm a) CanonPerformance)
  pnfCorrect verb p =
    do return (ifVerbose (do { print "The input formula:" ; D.display p }))
       t1 <- T.getClockTime
       let fastPdnf = pdnf' $! p
       t2 <- T.getClockTime
       let fastPdnfTime = diffTimes t2 t1
       return (ifVerbose (do { print ("The fast PDNF (computed in " ++ (show fastPdnfTime) ++ " milliseconds):") ; D.display fastPdnf }))
       t1 <- T.getClockTime
       let defaultPdnf = primeDNF $! p
       t2 <- T.getClockTime
       let defaultPdnfTime = diffTimes t2 t1
       return (ifVerbose (do { print ("The default PDNF (computed in " ++ (show defaultPdnfTime) ++ " milliseconds):") ; D.display defaultPdnf }))
       t1 <- T.getClockTime
       let fastPcnf = pcnf' $! p
       t2 <- T.getClockTime
       let fastPcnfTime = diffTimes t2 t1
       return (ifVerbose (do { print ("The fast PCNF (computed in " ++ (show fastPcnfTime) ++ " milliseconds):") ; D.display fastPcnf }))
       t1 <- T.getClockTime
       let defaultPcnf = primeCNF $! p
       t2 <- T.getClockTime
       let defaultPcnfTime = diffTimes t2 t1
       return (ifVerbose (do { print ("The default PCNF (computed in " ++ (show defaultPcnfTime) ++ " milliseconds):") ; D.display defaultPcnf }))
       let result = if defaultPdnf == fastPdnf && defaultPcnf == fastPcnf
                    then Right (sizeTriple p, (fastPdnfTime, sizeTriple fastPdnf), (fastPcnfTime, sizeTriple fastPcnf))
                    else Left p
       return (ifVerbose (do { print "The overall result is:" ; print result }))
       return result
    where ifVerbose act = if verb then act else (putStr "")

  pnfCorrectRepeat :: Verbose -> (Int, Int, Int) -> IO (PropForm Char)
  pnfCorrectRepeat verb (aCard, aSize, jSize) =
    do p <- randomCharProp (aCard, aSize, jSize)
       r <- pnfCorrect verb p
       q <- case r of
              Left p' -> return p'
              Right _ -> do print r
                            pnfCorrectRepeat verb (aCard, aSize, jSize)
       return q

-- performance tests

  pnfPerform :: (D.Display a, Show a, Ord a) => PropForm a -> IO CanonPerformance
  pnfPerform p =
    do let formSize = sizeTriple p
       t1 <- T.getClockTime
       let pdnfForm = pdnf' $! p
       let pdnfSize = sizeTriple $! pdnfForm
       t2 <- T.getClockTime
       let pdnfTime = diffTimes t2 t1
       t1 <- T.getClockTime
       let pcnfForm = pcnf' $! p
       let pcnfSize = sizeTriple $! pcnfForm
       t2 <- T.getClockTime
       let pcnfTime = diffTimes t2 t1
       return (formSize, (pdnfTime, pdnfSize), (pcnfTime, pcnfSize))

  pnfPerformRandom :: SizeTriple -> IO CanonPerformance
  pnfPerformRandom (aCard, aSize, jSize) =
    do p <- randomIntProp (aCard, aSize, jSize)
       r <- pnfPerform p
       return r

  pnfPerformRepeat :: SizeTriple -> IO ()
  pnfPerformRepeat st = do cp <- pnfPerformRandom st
                           print cp
                           x <- pnfPerformRepeat st
                           return x

---------------------------------------------------------------------------------------------------
-- new stuff ----------- move this into the right places ------------------------------------------
---------------------------------------------------------------------------------------------------

  onePrimFormTest :: IForm -> ()
  onePrimFormTest iform = let q = primForm iform
                              b1 = primeDNF (iDNF iform) == iDNF q
                              b2 = primeCNF (iCNF iform) == iCNF q
                          in if b1 && b2
                             then ()
                             else error ("onePrimFormTest dicovered an error for \n" ++ (show iform))

  primFormTesting :: Int -> Int -> Int -> IO ()
  primFormTesting atomNumber formLength averLineLen=
     do iform <- randomIForm atomNumber formLength averLineLen
        let b = onePrimFormTest iform
        putStr "."
        t <- primFormTesting atomNumber formLength averLineLen
        return t

  randomPrimForms :: Int -> Int -> Int -> IO ()
  randomPrimForms atomNumber formLen averLineLen =
     do iform <- randomIForm atomNumber formLen averLineLen
        let p = primForm iform
        let q = primForm iform
        putStr (show (formLength iform) ++ ":" ++ show (formLength p) ++ ":" ++ show (formLength q) ++ " ")
        t <- randomPrimForms atomNumber formLen averLineLen
        return t

  xprimTest :: ILine -> ILine -> Bool
  xprimTest line1 line2 = (xprim line1 line2) == (xprim' line1 line2)

  pairPrimTest :: ILine -> ILine -> Bool
  pairPrimTest line1 line2 = (pdnf == iDNF iform) && (pcnf == iCNF iform)
    where pdnf = primeDNF (DJ [iNLC line1, iNLC line2])
          pcnf = primeCNF (CJ [iNLD line1, iNLD line2])
          iform = orderForm (pairPrim line1 line2)

  xprimTesting :: Int -> Int -> IO ()
  xprimTesting atomNumber averLen =
    do line1 <- randomILine atomNumber averLen
       line2 <- randomILine atomNumber averLen
       let b = xprimTest line1 line2
       let s = if b then "." else error ("xprim and xprim' produce different results for "
                                       ++ (show line1) ++ " and " ++ (show line2))
       putStr s
       let b = pairPrimTest line1 line2
       let s = if b then "." else error ("pairPrim and primeDNF or primeCNF produce different PNFs for"
                                         ++ (show line1) ++ " and " ++ (show line2))
       putStr s
       t <- xprimTesting atomNumber averLen
       return t

  m2formTesting :: Int -> Int -> Int -> IO ()
  m2formTesting atomNumber formLen averLineLen =
     do iform <- randomIForm atomNumber formLen averLineLen
        let m = m2form iform
        putStr (show (formLength iform) ++ ":" ++ show (formLength m) ++ "  ")
        t <- m2formTesting atomNumber formLen averLineLen
        return t

  verbosePProcedure :: IForm -> IO ()
  verbosePProcedure iform = iter iform 0
    where iter iform step = do putStrLn ("step: " ++ (show step) ++
                                         "; atoms: " ++ (show (length (formIndices iform))) ++
                                         "; length: " ++ (show (formLength iform)) ++
                                         "; volume: " ++ (show (volume iform)) ++
                                         ": averageLineLength: " ++ (show (averageLineLength iform)))
                               let mform1 = m2form iform
                               let mform2 = orderForm mform1
                               r <- if mform2 == iform
                                    then putStrLn "DONE"
                                    else iter mform2 (step + 1)
                               return r

  pProcedureTesting :: Int -> Int -> Int -> IO ()
  pProcedureTesting atomNumber formLen averLineLen =
     do p <- randomIForm atomNumber formLen averLineLen
        verbosePProcedure p
        t <- pProcedureTesting atomNumber formLen averLineLen
        return t

-- Profiling - second version

-- testing the prime generation of IForms with random input IForms

  type Seconds = Double

  verboseRandomPrimeTest :: (Int,Int,Int) -> IO (Int,Int,Int,Seconds)
  -- ^ @randomPrimeTest (atomNum, formLen, averLineLen) = (atomNum', formLen', vol', secs')@
  verboseRandomPrimeTest (atomNum, formLen, averLineLen) =
     do iform <- randomIForm atomNum formLen averLineLen
        putStrLn "*** The random IForm is: ***"
        print iform
        putStrLn "*** Its prime IForm is: ***"
        t1 <- getCPUTime
        let pform = primForm $! iform
        print pform
        t2 <- getCPUTime
        putStrLn "*** Result of this test ***"
        putStr "Properties of the random IForm: "
        iformDiagnosis iform
        putStr "Properties of its prime IForm:  "
        iformDiagnosis pform
        let t = (fromIntegral (t2 - t1)) / 1000000000000 :: Seconds
        putStrLn ("Time to produce the prime IForm: " ++ (show t) ++ " seconds.")
        return (length (formIndices pform), formLength pform, volume pform, t)
     where iformDiagnosis :: IForm -> IO ()
           iformDiagnosis iform =  putStrLn ( "atomNumber = " ++ (show (length (formIndices iform))) ++
                                              "; formLength = " ++ (show (formLength iform)) ++
                                              "; volume = " ++ (show (volume iform)) ++
                                              "; averageLineLength = " ++ (show (averageLineLength iform)) )

  verboseRandomPrimeTesting :: (Int,Int,Int) -> Int -> IO (Int,Int,Seconds,Seconds,Seconds)
  -- ^ @verboseRandomPrimeTesting (atomNum, formLen, averLineLen) numberOfTests = (maxFormLen, averFormLen, maxTime, averTime, standDev)@
  verboseRandomPrimeTesting (atomNum, formLen, averLineLen) numberOfTests = iter [] numberOfTests
    where iter :: [(Int,Int,Int,Seconds)] -> Int -> IO (Int,Int,Seconds,Seconds,Seconds)
          iter qL n | n == 0    = do let (maxFormLen, averFormLen, maxTime, averTime, standDev) = evaluate qL
                                     D.printTextFrame $ D.textFrameBox $ D.correctTextFrame
                                      [ "All " ++ (show numberOfTests) ++ " tests have been performed: ",
                                        "  Parameters for the random IForms were:",
                                        "    atomNumber = " ++ (show atomNum),
                                        "    formLength = " ++ (show formLen),
                                        "    averageLineLength = " ++ (show averLineLen),
                                        "  Result of the test series:",
                                        "    numberOfTests = " ++ (show numberOfTests),
                                        "    maxFormLength = " ++ (show maxFormLen),
                                        "    averageFormLength = " ++ (show averFormLen),
                                        "    maxTime = " ++ (show maxTime) ++ " seconds",
                                        "    averageTime = " ++ (show averTime) ++ " seconds",
                                        "    standardTimeDeviation = " ++ (show standDev) ++ " seconds" ]
                                     return (maxFormLen, averFormLen, maxTime, averTime, standDev)
                    | otherwise = do putStrLn ("*** Test number " ++ (show (numberOfTests - n + 1)) ++
                                               " of " ++ (show numberOfTests) ++ ": ***")
                                     q <- verboseRandomPrimeTest (atomNum, formLen, averLineLen)
                                     iter (q:qL) (n - 1)
          evaluate :: [(Int,Int,Int,Seconds)] -> (Int,Int,Seconds,Seconds,Seconds)
          evaluate qL = let (formLenL, timeL) = unzip (map (\ (atomNum, formLen, vol, secs) -> (formLen, secs)) qL)
                        in ( maximum formLenL,
                             (sum formLenL) `div` (length formLenL),
                             maximum timeL,
                             meanValue timeL,
                             standDeviation timeL )

  meanValue :: [Seconds] -> Seconds
  meanValue timeL = (sum timeL) / (fromIntegral (length timeL))

  standDeviation :: [Seconds] -> Seconds
  standDeviation timeL = sqrt ( (sum (map (\ t -> (t - m)^2) timeL)) / (fromIntegral (length timeL)) )
    where m = meanValue timeL

  normSeconds :: Seconds -> Seconds
  normSeconds s = (fromIntegral (round (s * 1000))) / 1000