Commit 766128b4 authored by Camil Staps's avatar Camil Staps 🚀

Merge branch 'strict-maybe' into 'master'

Use strict maybe

See merge request !33
parents 3681da75 de0f3e7b
Pipeline #44571 passed with stage
in 43 seconds
......@@ -12,7 +12,6 @@ implementation module Gast.StdProperty
*/
import StdEnv
import StdMaybe
import Data.Func
from Math.Random import genRandInt
......@@ -47,7 +46,7 @@ instance /\ Bool Bool where (/\) x y = prop x /\ prop y
instance /\ Property Bool where (/\) x y = x /\ prop y
instance /\ Bool Property where (/\) x y = prop x /\ y
instance /\ Property Property
where (/\) x y = Prop ("(" +++ testname x +++ " /\\ " +++ testname y +++ ")") Nothing (and x y)
where (/\) x y = Prop ("(" +++ testname x +++ " /\\ " +++ testname y +++ ")") ?None (and x y)
where
and x y genState r
# r1 = testAnalysis r (evaluate x genState r)
......@@ -85,7 +84,7 @@ instance \/ Property Bool where (\/) x y = x \/ prop y
instance \/ Bool Property where (\/) x y = prop x \/ y
instance \/ Property Property
where
(\/) x y = Prop ("(" +++ testname x +++ " \\/ " +++ testname y +++ ")") Nothing (or x y)
(\/) x y = Prop ("(" +++ testname x +++ " \\/ " +++ testname y +++ ")") ?None (or x y)
where
or x y genState r = case testAnalysis r (evaluate x genState r) of
r=:{res=OK} -> [r]
......@@ -105,11 +104,11 @@ where
(===>) p q = (not p) || q
ExistsIn :: (x->p) [x] -> Property | Testable p & TestArg x
ExistsIn f l = Prop ("ExistsIn " +++ thunk_name_to_string f +++ " " +++ thunk_name_to_string l) Nothing p
ExistsIn f l = Prop ("ExistsIn " +++ thunk_name_to_string f +++ " " +++ thunk_name_to_string l) ?None p
where p rs r = [exists r [testAnalysis r (evaluate (f a) rs r)\\a <- l] MaxExists]
Exists :: (x->p) -> Property | Testable p & TestArg x
Exists f = Prop ("Exists " +++ thunk_name_to_string f) Nothing p
Exists f = Prop ("Exists " +++ thunk_name_to_string f) ?None p
where
p genState r =
[ exists
......@@ -150,37 +149,37 @@ where
= abort "Unknow result in testAnalysis"
ForAll :: !(x->p) -> Property | Testable p & TestArg x
ForAll f = Prop ("ForAll " +++ thunk_name_to_string f) Nothing (evaluate f)
ForAll f = Prop ("ForAll " +++ thunk_name_to_string f) ?None (evaluate f)
ForEach :: ![x] !(x->p) -> Property | Testable p & TestArg x
ForEach list f = Prop ("ForEach " +++ thunk_name_to_string list +++ " " +++ thunk_name_to_string f) Nothing (forAll f list)
ForEach list f = Prop ("ForEach " +++ thunk_name_to_string list +++ " " +++ thunk_name_to_string f) ?None (forAll f list)
(For) infixl 0 :: !(x->p) ![x] -> Property | Testable p & TestArg x
(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 Nothing \gs a -> affirm op (Other relName) x y gs {a & namePath=[name:a.namePath]}
check op x y = Prop name ?None \gs a -> affirm op (Other relName) x y gs {a & namePath=[name:a.namePath]}
where
name = thunk_name_to_string op
relName = concat [name, "{", thunk_to_module_name_string op, "}"]
(=.=) infix 4 :: !a !a -> Property | Eq, genShow{|*|}, gPrint{|*|} a
(=.=) x y = Prop "=.=" Nothing (affirm (==) Eq x y)
(=.=) x y = Prop "=.=" ?None (affirm (==) Eq x y)
(<.>) infix 4 :: !a !a -> Property | Eq, genShow{|*|}, gPrint{|*|} a
(<.>) x y = Prop "<.>" Nothing (affirm (<>) Ne x y)
(<.>) x y = Prop "<.>" ?None (affirm (<>) Ne x y)
(<.) infix 4 :: !a !a -> Property | Ord, genShow{|*|}, gPrint{|*|} a
(<.) x y = Prop "<." Nothing (affirm (<) Lt x y)
(<.) x y = Prop "<." ?None (affirm (<) Lt x y)
(<=.) infix 4 :: !a !a -> Property | Ord, genShow{|*|}, gPrint{|*|} a
(<=.) x y = Prop "<=." Nothing (affirm (<=) Le x y)
(<=.) x y = Prop "<=." ?None (affirm (<=) Le x y)
(>.) infix 4 :: !a !a -> Property | Ord, genShow{|*|}, gPrint{|*|} a
(>.) x y = Prop ">." Nothing (affirm (>) Gt x y)
(>.) x y = Prop ">." ?None (affirm (>) Gt x y)
(>=.) infix 4 :: !a !a -> Property | Ord, genShow{|*|}, gPrint{|*|} a
(>=.) x y = Prop ">=." Nothing (affirm (>=) Ge x y)
(>=.) x y = Prop ">=." ?None (affirm (>=) Ge x y)
affirm :: !(a b->Bool) !Relation a b .GenState !.Admin -> [Admin] | genShow{|*|}, gPrint{|*|} a & genShow{|*|}, gPrint{|*|} b
affirm op rel x y rs admin
......@@ -198,7 +197,7 @@ affirm op rel x y rs admin
}
(ForAndGen) infixl 0 :: !(x->p) ![x] -> Property | Testable p & TestArg x
(ForAndGen) p list = Prop (thunk_name_to_string p +++ " ForAndGen " +++ thunk_name_to_string list) Nothing (evaluate p)
(ForAndGen) p list = Prop (thunk_name_to_string p +++ " ForAndGen " +++ thunk_name_to_string list) ?None (evaluate p)
where
evaluate f rs result =
forAll f
......@@ -208,20 +207,20 @@ where
classify :: !Bool l !p -> Property | Testable p & genShow{|*|} l
classify c l p
| c = Prop (testname p) Nothing (\rs r = evaluate p rs {r & labels = [show1 l:r.labels]})
= Prop (testname p) Nothing (evaluate p)
| c = Prop (testname p) ?None (\rs r = evaluate p rs {r & labels = [show1 l:r.labels]})
= Prop (testname p) ?None (evaluate p)
label :: !l !p -> Property | Testable p & genShow{|*|} l
label l p = Prop (testname p) Nothing (\rs r = evaluate p rs {r & labels = [show1 l:r.labels]})
label l p = Prop (testname p) ?None (\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) Nothing (\rs r -> evaluate p rs {r & namePath=[toString n:r.namePath]})
name n p = Prop (toString n) ?None (\rs r -> evaluate p rs {r & namePath=[toString n:r.namePath]})
location_and_name :: !TestLocation !n !p -> Property | Testable p & toString n
location_and_name l n p = Prop (toString n) (Just l) \rs r -> evaluate p rs {r & namePath=[toString n:r.namePath]}
location_and_name l n p = Prop (toString n) (?Just l) \rs r -> evaluate p rs {r & namePath=[toString n:r.namePath]}
limitNrOfRecFieldValues :: !(Map (TypeName, RecFieldName) Int) !p -> Property | Testable p
limitNrOfRecFieldValues limits p = Prop (testname p) Nothing (\rs r = evaluate p rs {Admin| r & recFieldValueNrLimits = limits})
limitNrOfRecFieldValues limits p = Prop (testname p) ?None (\rs r = evaluate p rs {Admin| r & recFieldValueNrLimits = limits})
instance ~ Bool where ~ b = not b
......@@ -237,6 +236,6 @@ instance ~ Property
where ~ (Prop n m p) = Prop ("~" +++ n) m (\rs r = let r` = testAnalysis r (p rs r) in [{r` & res = ~r`.res}])
approxEqual :: !a !a !a -> Property | abs, Ord, -, genShow{|*|}, gPrint{|*|} a
approxEqual err x y = Prop "approximately equals" Nothing
approxEqual err x y = Prop "approximately equals" ?None
(affirm (\x y -> abs (x - y) <= err)
(Other $ concat ["approximately equals (error = ", printToString err, ")"]) x y)
......@@ -11,7 +11,6 @@ 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
......@@ -35,7 +34,7 @@ newAdmin :: Admin
derive gLess Result
instance == Result
:: Property = Prop String (Maybe TestLocation) (GenState Admin -> [Admin])
:: Property = Prop String (?TestLocation) (GenState Admin -> [Admin])
prop :: a -> Property | Testable a
......@@ -46,8 +45,8 @@ where
evaluate :: !a GenState !Admin -> [Admin]
testname :: a -> String
testlocation :: a -> Maybe TestLocation
testlocation _ = Nothing
testlocation :: a -> ?TestLocation
testlocation _ = ?None
instance Testable Bool
instance Testable Result
......@@ -119,8 +118,8 @@ generateAll :: !GenState -> [a] | ggen{|*|} a //& genType{|*|} a
}
:: GastEvent
= GE_TestStarted !(Maybe TestLocation) !String
| GE_TestFinished !(Maybe TestLocation) !String !TestsResult ![CounterExampleRes] ![(String,Int)]
= GE_TestStarted !(?TestLocation) !String
| GE_TestFinished !(?TestLocation) !String !TestsResult ![CounterExampleRes] ![(String,Int)]
| GE_CounterExample !CounterExampleRes
| GE_Tick !Int !Admin
......@@ -134,8 +133,8 @@ generateAll :: !GenState -> [a] | ggen{|*|} a //& genType{|*|} a
:: PrintConfig =
{ everyOutput :: Int Admin -> String
, counterExampleOutput :: CounterExampleRes -> String
, beforeStartOutput :: (Maybe TestLocation) String -> String
, resultOutput :: (Maybe TestLocation) String TestsResult [CounterExampleRes] [(String, Int)] -> String
, beforeStartOutput :: (?TestLocation) String -> String
, resultOutput :: (?TestLocation) String TestsResult [CounterExampleRes] [(String, Int)] -> String
}
printEvents :: PrintConfig [GastEvent] -> [String]
......
......@@ -60,7 +60,7 @@ where
where
genState` = {GenState| genState & recFieldValueNrLimits = admin.Admin.recFieldValueNrLimits}
testname f = thunk_name_to_string f
testlocation f = Just {moduleName=Just (thunk_to_module_name_string f)}
testlocation f = ?Just {moduleName=Just (thunk_to_module_name_string f)}
instance Testable [a] | Testable a
where
......@@ -173,7 +173,7 @@ testEventsPrintConfig =
noCounterExampleOutput :: CounterExampleRes -> String
noCounterExampleOutput _ = ""
noBeforeOutput :: !(Maybe TestLocation) !String -> String
noBeforeOutput :: !(?TestLocation) !String -> String
noBeforeOutput _ _ = ""
noEveryOutput :: !Int Admin -> String
......@@ -197,7 +197,7 @@ where
showFailedAssertion :: !(!FailedAssertion, !String, !String) -> [String]
showFailedAssertion (ExpectedRelation _ rel _, x, y) = ["not (", x, " ", toString rel, " ", y, ")\n"]
humanReadableResOutput :: Bool (Maybe TestLocation) String TestsResult [CounterExampleRes] [(String, Int)] -> String
humanReadableResOutput :: Bool (?TestLocation) String TestsResult [CounterExampleRes] [(String, Int)] -> String
humanReadableResOutput addWhite _ name {maxTests, nRej, resultType} _ labels = withBlank $ showName True name +++ resStr
where
resStr = case resultType of
......@@ -237,21 +237,24 @@ 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 :: !(Maybe TestLocation) !String -> String
jsonEventStart loc name = toString (toJSON {StartEvent | name=name, location=loc}) +++ "\n"
jsonEventStart :: !(?TestLocation) !String -> String
jsonEventStart loc name = toString (toJSON {StartEvent | name=name, location=loc`}) +++ "\n"
where
loc` = case loc of ?Just l -> Just l; _ -> Nothing
jsonEventEnd :: !(Maybe TestLocation) !String !TestsResult ![CounterExampleRes] ![(String, Int)] -> String
jsonEventEnd :: !(?TestLocation) !String !TestsResult ![CounterExampleRes] ![(String, Int)] -> String
jsonEventEnd loc name res counterExamples labels = toString (toJSON endEvent) +++ "\n"
where
endEvent =
{ name = showName False name
, location = loc
, location = loc`
, event = eventType
, message = concat
[ humanReadableResOutput False loc name res counterExamples labels
: map (humanReadableCEOutput False False) counterExamples
]
}
loc` = case loc of ?Just l -> Just l; _ -> Nothing
eventType = case res.resultType of
Proof _ -> Passed
......
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