include counter examples in json end event messages

Libraries/Gast/Testable.icl

@@ -22,9 +22,11 @@ instance == Result where (==) x y = x===y
 newAdmin :: Admin
 newAdmin = {res=Undef, labels=[], args=[], name=[], mes = []}
 
-instance Testable Bool where evaluate b genState result=:{args} = [{result & args = reverse args, res = if b OK CE}]
+instance Testable Bool where
+    evaluate b genState result=:{Admin| args} = [{result & args = reverse args, res = if b OK CE}]
 
-instance Testable Result where evaluate r genState result=:{args} = [{result & args = reverse args, res = r}]
+instance Testable Result where
+    evaluate r genState result=:{Admin| args} = [{result & args = reverse args, res = r}]
 
 instance Testable Property
 where evaluate (Prop p) genState result = p genState result
@@ -40,11 +42,11 @@ prop :: a -> Property | Testable a
 prop p = Prop (evaluate p)
 
 forAll :: !(a->b) ![a] GenState !Admin -> [Admin] | Testable b & TestArg a
-forAll f []   genState r=:{args} = [{r & args = reverse args, res = OK}]				// to handle empty sets of values
+forAll f []   genState r=:{Admin| args} = [{r & args = reverse args, res = OK}]				// to handle empty sets of values
 forAll f list genState r = diagonal [apply f a genState r \\ a<-list ] // copy the genState
 
 apply :: !(a->b) a GenState !Admin -> [Admin] | Testable b & TestArg a
-apply f a genState r = evaluate (f a) genState {r & args = [show1 a:r.args]}
+apply f a genState r = evaluate (f a) genState {Admin| r & args = [show1 a:r.Admin.args]}
 
 diagonal :: [[a]] -> [a]
 diagonal list = f 1 2 list []
@@ -70,16 +72,16 @@ derive bimap [], (,), (,,), (,,,), (,,,,), (,,,,,)
  =	{ maxTests	           :: Int
 	, maxArgs	           :: Int
 	, everyOutput		   :: Int Admin [String] -> [String]
-    , counterExampleOutput :: Int Int Int [String] [String] [String] -> [String]
+    , counterExampleOutput :: CounterExample [String] -> [String]
     , beforeStartOutput    :: [String] -> [String]
-    , resultOutput         :: TestsResult [(!String, !Int)] [String] -> [String]
+    , resultOutput         :: TestsResult [CounterExample] [(!String, !Int)] [String] -> [String]
 	, fails		           :: Int
 	, randoms	           :: [Int]
 	, genState	           :: GenState
 	}
 
 /**
- * Represents the combined results of all tests for a single property.
+ * The combined results of all tests for a single property.
  * This is in contrast to {{Result}} which represents the result of a single test.
  */
 :: TestsResult = { maxTests   :: !Int        //* Maximum number of tests
@@ -87,7 +89,7 @@ derive bimap [], (,), (,,), (,,,), (,,,,), (,,,,,)
                  , resultType :: !ResultType //* Type of the result
                  }
 /**
- * Represent the type of the combined result, together with information
+ * The type of the combined result, together with information
  * specific to that type of result.
  */
 :: ResultType = Proof           !Int                 //* Proof by exhaustive testing: nTests
@@ -96,6 +98,16 @@ derive bimap [], (,), (,,), (,,,), (,,,,), (,,,,,)
               | Undefined       !Int                 //* Undefined result: nUnd
               | NoTests         !Int !Int !Int       //* No tests performed: maxArgs nTests nUnd
 
+/**
+ * A counter examples.
+ */
+:: CounterExample = { maxTests :: !Int      //* Maximal number of tests for run in which counter example is found
+                    , nTests   :: !Int      //* maxTests MINUS number of test at which counter example is found
+                    , nE       :: !Int      //* Number of counter example
+                    , args     :: ![String] //* Arguments used for test
+                    , name     :: ![String] //* Name of property
+                    }
+
 verboseConfig
  =	{ maxTests	           = NrOfTest
 	, maxArgs	           = 2*NrOfTest
@@ -108,7 +120,7 @@ verboseConfig
 	, genState	           = genState
 	}
 
-verboseEvery n r c = [blank,toString n,":":showArgs r.args (r.mes++c)]
+verboseEvery n r c = [blank,toString n,":":showArgs r.Admin.args (r.mes++c)]
 
 traceConfig
  =	{ maxTests             = 100
@@ -121,7 +133,7 @@ traceConfig
 	, randoms	           = aStream
 	, genState	           = genState
 	}
-traceEvery n r c = [toString n,":":showArgs r.args ["\n":r.mes++c]]
+traceEvery n r c = [toString n,":":showArgs r.Admin.args ["\n":r.mes++c]]
 
 blank :: String
 blank =: { createArray len ' ' & [0] = '\r', [len-1] = '\r' } where len = 81
@@ -181,30 +193,28 @@ animate2 n r c
 		= ["\r       \r",toString n," ":c]
 		= c
 
-noCounterExampleOutput :: Int Int Int [String] [String] [String] -> [String]
-noCounterExampleOutput _ _ _ _ _ acc = acc
+noCounterExampleOutput :: CounterExample [String] -> [String]
+noCounterExampleOutput _ acc = acc
 
 noBeforeOutput :: ![String] -> [String]
 noBeforeOutput _ = []
 
 noEveryOutput _ _ c = ["":c] // FIXME: empty string required to prevent stack overflow, why?
 
-humanReadableCEOutput :: Int Int Int [String] [String] [String] -> [String]
-humanReadableCEOutput maxTests nTests nE args name acc =
-    [ "\r"
-    : showName True
-               name
-               [ "Counterexample "
-               , toString (nE+1)
-               , " found after "
-               , pluralisen English (maxTests - nTests + 1) "test"
-               , ":"
-               : showArgs args ["\n":acc]
-               ]
-    ]
-
-humanReadableResOutput :: Bool TestsResult [(String, Int)] [String] -> [String]
-humanReadableResOutput addWhite {maxTests, nRej, resultType} labels name = withBlank $ showName True name resStr
+humanReadableCEOutput :: CounterExample [String] -> [String]
+humanReadableCEOutput {maxTests, nTests, nE, args, name} acc =
+    showName True
+             name
+             [ "Counterexample "
+             , toString (nE+1)
+             , " found after "
+             , pluralisen English (maxTests - nTests + 1) "test"
+             , ":"
+             : showArgs args ["\n":acc]
+             ]
+
+humanReadableResOutput :: Bool TestsResult [CounterExample] [(String, Int)] [String] -> [String]
+humanReadableResOutput addWhite {maxTests, nRej, resultType} _ labels name = withBlank $ showName True name resStr
 where
     resStr = case resultType of
         Proof nTests -> ["Proof: ", msgStr: conclude addWhite nTests 0 labels]
@@ -253,12 +263,12 @@ where
 jsonEventStart :: ![String] -> [String]
 jsonEventStart name = [toString $ toJSON {StartEvent | name = concat $ showName False name []}, "\n"]
 
-jsonEventEnd :: TestsResult [(String, Int)] [String] -> [String]
-jsonEventEnd res labels name = [toString (toJSON endEvent) +++ "\n"]
+jsonEventEnd :: TestsResult [CounterExample] [(String, Int)] [String] -> [String]
+jsonEventEnd res counterExamples labels name = [toString (toJSON endEvent) +++ "\n"]
 where
     endEvent = { name    = concat $ showName False name []
                , event   = eventType
-               , message = concat $ humanReadableResOutput False res labels []
+               , message = concat $ foldl (flip humanReadableCEOutput) (humanReadableResOutput False res counterExamples labels []) counterExamples
                }
 
     eventType = case res.resultType of
@@ -368,14 +378,15 @@ testConfig :: RandomStream Config p -> [String] | Testable p
 testConfig rs {maxTests,maxArgs,everyOutput,counterExampleOutput,beforeStartOutput,resultOutput,fails,genState} p
     // we first have to evaluate to get the name
     # res = evaluate p genState newAdmin
-    = [concat $ beforeStartOutput (hd res).Admin.name : analyse res maxTests maxArgs 0 0 0 [] []]
+    = [concat $ beforeStartOutput (hd res).Admin.name : analyse res maxTests maxArgs 0 0 0 [] [] []]
 where
-	analyse :: ![.Admin] !Int !Int !Int !Int !Int ![(String,Int)] ![String] -> [String]
-    analyse results nTests nArgs nRej nUnd nE labels name =
+	analyse :: ![.Admin] !Int !Int !Int !Int !Int [CounterExample] ![(String,Int)] ![String] -> [String]
+    analyse results nTests nArgs nRej nUnd nE counterExamples labels name =
         case analyse` results nTests nArgs nRej nUnd nE of
             // testing of property finished
             Just resType -> resultOutput
                 {maxTests = maxTests, nRej = nRej, resultType = resType}
+                counterExamples
                 labels
                 name
             // continue with testing property
@@ -383,22 +394,32 @@ where
                 let [res:rest] = results in
                 everyOutput (maxTests-nTests+1) res
                   (	case res.res of
-                     OK 	= analyse rest (nTests-1) (nArgs-1) nRej nUnd nE (admin res.labels labels) res.Admin.name
-                     Pass	= analyse rest (nTests-1) (nArgs-1) nRej nUnd nE (admin res.labels labels) res.Admin.name // NOT YET CORRECT ?
-                     CE		= counterExampleOutput maxTests nTests nE res.args res.Admin.name more
-                              where
+                     OK 	= analyse rest (nTests-1) (nArgs-1) nRej nUnd nE
+                                      counterExamples (admin res.labels labels) res.Admin.name
+                     Pass	= analyse rest (nTests-1) (nArgs-1) nRej nUnd nE
+                                      counterExamples (admin res.labels labels) res.Admin.name // NOT YET CORRECT ?
+                     CE		= counterExampleOutput counterExample more
+                            where
+                                counterExample = { maxTests = maxTests
+                                                 , nTests   = nTests
+                                                 , nE       = nE
+                                                 , args     = res.Admin.args
+                                                 , name     = res.Admin.name
+                                                 }
+
                                 more | nE+1<fails
                                     = analyse rest (nTests-1) (nArgs-1) nRej nUnd (nE+1)
-                                              (admin res.labels labels) res.Admin.name
+                                              [counterExample: counterExamples] (admin res.labels labels) res.Admin.name
                                     = resultOutput
                                         { maxTests   = maxTests
                                         , nRej       = nRej
                                         , resultType = CounterExamples (nTests - 1) nUnd (nE + 1)
                                         }
+                                        [counterExample: counterExamples] 
                                         (admin res.labels labels)
                                         res.Admin.name 
-                     Rej	= analyse rest nTests (nArgs-1) (nRej+1) nUnd     nE labels res.Admin.name
-                     Undef	= analyse rest nTests (nArgs-1) nRej     (nUnd+1) nE labels res.Admin.name
+                     Rej	= analyse rest nTests (nArgs-1) (nRej+1) nUnd     nE counterExamples labels res.Admin.name
+                     Undef	= analyse rest nTests (nArgs-1) nRej     (nUnd+1) nE counterExamples labels res.Admin.name
                             = abort "Error in Gast: analyse; missing case for result\n"
                   )