Verified Commit a9dcc9cd authored by Camil Staps's avatar Camil Staps 🚀

Keep track of source location; add support in exposeProperties to add source location

parent 2968e7e1
Pipeline #27777 failed with stage
in 44 seconds
......@@ -5,6 +5,7 @@ definition module Gast.CommandLine
* {{`Testing.Options`}}.
*/
from StdMaybe import :: Maybe
from Gast.Testable import class Testable, :: Testoption, :: PrintOption
class getOptions a :: a -> [Testoption]
......@@ -18,14 +19,22 @@ instance getOptions ([Testoption], a, b)
instance getPrintOptions (a, [PrintOption], b)
/**
* Wrap a TestableWithOptions in an existential type to easily build
* quasi-heterogeneous lists of properties.
* Wrap a Testable in an existential type to easily build quasi-heterogeneous
* lists of properties.
*/
:: ExposedProperty = E.p: EP p & Testable, getOptions p
:: ExposedProperty = E.p: EP !p & Testable, getOptions p
instance Testable ExposedProperty
instance getOptions ExposedProperty
/**
* Like ExposedProperty, but with location information (filename and line number).
*/
:: ExposedLocatedProperty = E.p: EPLoc !(Maybe String) !(Maybe Int) !p & Testable, getOptions p
instance Testable ExposedLocatedProperty
instance getOptions ExposedLocatedProperty
/**
* Expose a set of Gast properties as a CLI application.
*
......
......@@ -41,6 +41,15 @@ where
instance getOptions ExposedProperty where getOptions (EP p) = getOptions p
instance Testable ExposedLocatedProperty
where
evaluate (EPLoc f l p) g a = evaluate p g {a & meta.sourceLocation=(f,l)}
testname (EPLoc _ _ p) = testname p
testfile (EPLoc f _ _) = f
testline (EPLoc _ l _) = l
instance getOptions ExposedLocatedProperty where getOptions (EPLoc _ _ p) = getOptions p
exposeProperties :: ![PrintOption] ![Testoption] ![a] !*World -> *World | Testable, getOptions a
exposeProperties printopts globopts ps w
# ([_:opts], w) = getCommandLine w
......@@ -89,9 +98,9 @@ where
stream pc [ge:ges] io w
# io = foldl (\io ev -> snd $ fflush $ io <<< ev) io $ printEvents pc [ge]
# w = case ge of
GE_TestFinished _ {resultType=CounterExpls _ _ _} _ _ -> setReturnCode 1 w
GE_TestFinished _ {resultType=Undefined _} _ _ -> setReturnCode 1 w
_ -> w
GE_TestFinished _ _ {resultType=CounterExpls _ _ _} _ _ -> setReturnCode 1 w
GE_TestFinished _ _ {resultType=Undefined _} _ _ -> setReturnCode 1 w
_ -> w
= stream pc ges io w
stream _ [] io w = (io,w)
......
......@@ -158,7 +158,7 @@ ForEach list f = Prop ("ForEach " +++ thunk_name_to_string list +++ " " +++ thun
(For) p list = ForEach list p
check :: !(a b -> Bool) !a !b -> Property | genShow{|*|}, gPrint{|*|} a & genShow{|*|}, gPrint{|*|} b
check op x y = Prop name (\gs a -> affirm op (Other relName) x y gs {a & namePath=[name:a.namePath]})
check op x y = Prop name (\gs a -> affirm op (Other relName) x y gs {a & meta.namePath=[name:a.meta.namePath]})
where
name = thunk_name_to_string op
relName = concat [name, "{", thunk_to_module_name_string op, "}"]
......@@ -211,7 +211,7 @@ label :: !l !p -> Property | Testable p & genShow{|*|} l
label l p = Prop (testname p) (\rs r = evaluate p rs {r & labels = [show1 l:r.labels]})
name :: !n !p -> Property | Testable p & toString n
name n p = Prop (toString n) (\rs r -> evaluate p rs {r & namePath=[toString n:r.namePath]})
name n p = Prop (toString n) (\rs r -> evaluate p rs {r & meta.namePath=[toString n:r.meta.namePath]})
limitNrOfRecFieldValues :: !(Map (TypeName, RecFieldName) Int) !p -> Property | Testable p
limitNrOfRecFieldValues limits p = Prop (testname p) (\rs r = evaluate p rs {Admin| r & recFieldValueNrLimits = limits})
......
......@@ -11,6 +11,7 @@ definition module Gast.Testable
pieter@cs.ru.nl
*/
from StdMaybe import :: Maybe(Nothing)
import Gast.GenLibTest
from Gast.StdProperty import ::Property // for instance of testable
import Gast.Gen
......@@ -23,11 +24,16 @@ from Text.GenPrint import class PrintOutput, :: PrintState, generic gPrint
{ labels :: ![String]
, args :: ![String]
, argsRepresentation :: ![String]
, namePath :: ![String]
, res :: !Result
, failedAssertions :: ![(FailedAssertion, String, String)] //* Failed assertion & string representation of args
, recFieldValueNrLimits :: !Map (TypeName, RecFieldName) Int //* Restricts the number of values generated for record fields
, meta :: AdminMeta // Keep unboxed for efficiency!
}
:: AdminMeta =
{ namePath :: ![String]
, sourceLocation :: !(!Maybe String,!Maybe Int) //* source file name and line number
}
:: Result = Undef | Rej | Pass | OK | CE
newAdmin :: Admin
......@@ -44,6 +50,12 @@ where
evaluate :: !a GenState !Admin -> [Admin]
testname :: a -> String
testfile :: a -> Maybe String
testfile _ = Nothing
testline :: a -> Maybe Int
testline _ = Nothing
instance Testable Bool
instance Testable Result
instance Testable Property
......@@ -113,8 +125,8 @@ generateAll :: !GenState -> [a] | ggen{|*|} a //& genType{|*|} a
}
:: GastEvent
= GE_TestStarted String
| GE_TestFinished String TestsResult [CounterExampleRes] [(String,Int)]
= GE_TestStarted !String !(Maybe String, Maybe Int)
| GE_TestFinished !String !(Maybe String, Maybe Int) !TestsResult ![CounterExampleRes] ![(String,Int)]
| GE_CounterExample CounterExampleRes
| GE_Tick Int Admin
......@@ -126,10 +138,10 @@ generateAll :: !GenState -> [a] | ggen{|*|} a //& genType{|*|} a
| OutputTestEvents //* output test results as event specified in clean-platform {{Testing.TestEvents}}
:: PrintConfig =
{ everyOutput :: Int Admin -> String
, counterExampleOutput :: CounterExampleRes -> String
, beforeStartOutput :: String -> String
, resultOutput :: String TestsResult [CounterExampleRes] [(String, Int)] -> String
{ everyOutput :: !Int Admin -> String
, counterExampleOutput :: !CounterExampleRes -> String
, beforeStartOutput :: !String (Maybe String, Maybe Int) -> String
, resultOutput :: !String (Maybe String, Maybe Int) TestsResult [CounterExampleRes] [(String, Int)] -> String
}
printEvents :: PrintConfig [GastEvent] -> [String]
......
......@@ -33,8 +33,8 @@ instance == Result where (==) x y = x===y
newAdmin :: Admin
newAdmin = { res=Undef, labels=[], args=[], argsRepresentation = [], failedAssertions = []
, namePath = []
, recFieldValueNrLimits = 'Data.Map'.newMap
, meta = {namePath=[], sourceLocation=(Nothing,Nothing)}
}
instance Testable Bool where
......@@ -61,7 +61,7 @@ where
instance Testable [a] | Testable a
where
evaluate list genState admin = diagonal [ evaluate x genState admin \\ x<-list ] // copy the genState
evaluate list genState admin = diagonal [ evaluate x genState {admin & meta.sourceLocation=(testfile x,testline x)} \\ x<-list ] // copy the genState
testname xs = "[" +++ join "," (map testname xs) +++ "]"
prop :: a -> Property | Testable a
......@@ -109,10 +109,10 @@ printEvents pc [ge:ges] = case s of
s -> [s:printEvents pc ges]
where
s = case ge of
GE_TestStarted n -> pc.beforeStartOutput n
GE_TestFinished n r ces labels -> pc.resultOutput n r ces labels
GE_CounterExample ce -> pc.counterExampleOutput ce
GE_Tick n adm -> pc.everyOutput n adm
GE_TestStarted n loc -> pc.beforeStartOutput n loc
GE_TestFinished n loc r ces labels -> pc.resultOutput n loc r ces labels
GE_CounterExample ce -> pc.counterExampleOutput ce
GE_Tick n adm -> pc.everyOutput n adm
printEvents _ [] = []
defaultTestConfig =
......@@ -170,8 +170,8 @@ testEventsPrintConfig =
noCounterExampleOutput :: CounterExampleRes -> String
noCounterExampleOutput _ = ""
noBeforeOutput :: !String -> String
noBeforeOutput _ = ""
noBeforeOutput :: !String !(Maybe String, Maybe Int) -> String
noBeforeOutput _ _ = ""
noEveryOutput :: !Int Admin -> String
noEveryOutput n _ = ""
......@@ -194,8 +194,8 @@ where
showFailedAssertion :: !(!FailedAssertion, !String, !String) -> [String]
showFailedAssertion (ExpectedRelation _ rel _, x, y) = ["not (", x, " ", toString rel, " ", y, ")\n"]
humanReadableResOutput :: Bool String TestsResult [CounterExampleRes] [(String, Int)] -> String
humanReadableResOutput addWhite name {maxTests, nRej, resultType} _ labels = withBlank $ showName True name +++ resStr
humanReadableResOutput :: Bool String (Maybe String, Maybe Int) TestsResult [CounterExampleRes] [(String, Int)] -> String
humanReadableResOutput addWhite name _ {maxTests, nRej, resultType} _ labels = withBlank $ showName True name +++ resStr
where
resStr = case resultType of
Proof nTests -> "Proof: " +++ msgStr +++ conclude nTests 0 labels
......@@ -234,17 +234,19 @@ where
showLabels 0 [(lab,n):rest] = ["\n",lab,": ",toString n:showLabels 0 rest]
showLabels ntests [(lab,n):rest] = ["\n",lab,": ",toString n," (",toString (toReal (n*100)/toReal ntests),"%)":showLabels ntests rest]
jsonEventStart :: !String -> String
jsonEventStart name = toString (toJSON {StartEvent | name=name}) +++ "\n"
jsonEventStart :: !String !(!Maybe String, !Maybe Int) -> String
jsonEventStart name (filename,line) = toString (toJSON {StartEvent | name=name, filename=filename, line=line}) +++ "\n"
jsonEventEnd :: String TestsResult [CounterExampleRes] [(String, Int)] -> String
jsonEventEnd name res counterExamples labels = toString (toJSON endEvent) +++ "\n"
jsonEventEnd :: !String !(!Maybe String, !Maybe Int) !TestsResult ![CounterExampleRes] ![(String, Int)] -> String
jsonEventEnd name loc=:(filename,line) res counterExamples labels = toString (toJSON endEvent) +++ "\n"
where
endEvent =
{ name = showName False name
, event = eventType
, message = concat
[ humanReadableResOutput False name res counterExamples labels
{ name = showName False name
, filename = filename
, line = line
, event = eventType
, message = concat
[ humanReadableResOutput False name loc res counterExamples labels
: map (humanReadableCEOutput False False) counterExamples
]
}
......@@ -346,15 +348,19 @@ testEventsn n rs p = printEvents testEventsPrintConfig $ testConfig rs { default
testConfig :: RandomStream Config p -> [GastEvent] | Testable p
testConfig rs {maxTests,maxArgs,fails,genState} p
# res = evaluate p genState newAdmin
= [GE_TestStarted (testname p):analyse res maxTests maxArgs 0 0 0 [] []]
= [GE_TestStarted (testname p) first_loc:analyse Nothing first_step maxTests maxArgs 0 0 0 [] []]
where
analyse :: ![.Admin] !Int !Int !Int !Int !Int [CounterExampleRes] ![(String,Int)] -> [GastEvent]
analyse results nTests nArgs nRej nUnd nE counterExamples labels =
first_step = evaluate p genState newAdmin
first_loc = case first_step of
[adm:_] -> adm.meta.sourceLocation
_ -> (Nothing,Nothing)
analyse :: !(Maybe Admin) ![.Admin] !Int !Int !Int !Int !Int [CounterExampleRes] ![(String,Int)] -> [GastEvent]
analyse last results nTests nArgs nRej nUnd nE counterExamples labels =
case analyse` results nTests nArgs nRej nUnd nE of
// testing of property finished
Just resType -> [GE_TestFinished
(testname p)
(testname p) (case last of Just adm -> adm.meta.sourceLocation; Nothing -> first_loc)
{maxTests = maxTests, nRej = nRej, resultType = resType}
counterExamples
labels]
......@@ -362,8 +368,8 @@ where
Nothing ->
let [res:rest] = results in
[GE_Tick (maxTests-nTests+1) res:case res.res of
OK -> analyse rest (nTests-1) (nArgs-1) nRej nUnd nE counterExamples (admin res.labels labels)
Pass -> analyse rest (nTests-1) (nArgs-1) nRej nUnd nE counterExamples (admin res.labels labels) // NOT YET CORRECT ?
OK -> analyse (Just res) rest (nTests-1) (nArgs-1) nRej nUnd nE counterExamples (admin res.labels labels)
Pass -> analyse (Just res) rest (nTests-1) (nArgs-1) nRej nUnd nE counterExamples (admin res.labels labels) // NOT YET CORRECT ?
CE -> [GE_CounterExample counterExample:more]
with
counterExample =
......@@ -372,21 +378,21 @@ where
, nE = nE
, args = res.Admin.args
, argsRepresentation = res.Admin.argsRepresentation
, name = let n = testname p in join "." [n:dropWhile ((==) n) (reverse res.namePath)]
, name = let n = testname p in join "." [n:dropWhile ((==) n) (reverse res.meta.namePath)]
, failedAssertions = res.Admin.failedAssertions
}
more | nE+1<fails
= analyse rest (nTests-1) (nArgs-1) nRej nUnd (nE+1) [counterExample: counterExamples] (admin res.labels labels)
= analyse (Just res) rest (nTests-1) (nArgs-1) nRej nUnd (nE+1) [counterExample: counterExamples] (admin res.labels labels)
= [GE_TestFinished
(testname p)
(testname p) res.meta.sourceLocation
{ maxTests = maxTests
, nRej = nRej
, resultType = CounterExpls (nTests - 1) nUnd (nE + 1)
}
[counterExample: counterExamples]
(admin res.labels labels)]
Rej -> analyse rest nTests (nArgs-1) (nRej+1) nUnd nE counterExamples labels
Undef -> analyse rest nTests (nArgs-1) nRej (nUnd+1) nE counterExamples labels
Rej -> analyse (Just res) rest nTests (nArgs-1) (nRej+1) nUnd nE counterExamples labels
Undef -> analyse (Just res) rest nTests (nArgs-1) nRej (nUnd+1) nE counterExamples labels
_ -> abort "Error in Gast: analyse; missing case for result\n"
]
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment