@@ -27,6 +27,9 @@ module Test.QuickCheck.DynamicLogic (
2727 forAllDL ,
2828 forAllMappedDL ,
2929 forAllUniqueDL ,
30+ forAllDLS ,
31+ forAllMappedDLS ,
32+ forAllUniqueDLS ,
3033 DL. DynLogicModel (.. ),
3134 module Test.QuickCheck.DynamicLogic.Quantify ,
3235) where
@@ -133,24 +136,21 @@ forAllNonVariableQ q = DL $ \s k -> DL.forAllQ (hasNoVariablesQ q) $ \(HasNoVari
133136runDL :: Annotated s -> DL s () -> DL. DynFormula s
134137runDL s dl = (unDL dl s $ \ _ _ -> DL. passTest)
135138
136- -- TODO: We probably want versions of these three functions that take an `s` so that you can write DL
137- -- properties that are only true in a specific starting state rather than a random starting state.
138-
139139forAllUniqueDL
140140 :: (DL. DynLogicModel s , Testable a )
141141 => DL s ()
142142 -> (Actions s -> a )
143143 -> Property
144144forAllUniqueDL d p =
145- forAllBlind initialState $ \ st -> DL. forAllUniqueScripts st (runDL ( Metadata mempty st) d) p
145+ forAllBlind initialState $ \ st -> forAllUniqueDLS st d p
146146
147147forAllDL
148148 :: (DL. DynLogicModel s , Testable a )
149149 => DL s ()
150150 -> (Actions s -> a )
151151 -> Property
152152forAllDL d p =
153- forAllBlind initialState $ \ st -> DL. forAllScripts st (runDL ( Metadata mempty st) d) p
153+ forAllBlind initialState $ \ st -> forAllDLS st d p
154154
155155forAllMappedDL
156156 :: (DL. DynLogicModel s , Testable a )
@@ -161,5 +161,34 @@ forAllMappedDL
161161 -> (srep -> a )
162162 -> Property
163163forAllMappedDL to from fromScript d prop =
164- forAll initialState $ \ st ->
165- DL. forAllMappedScripts st to from (runDL (Metadata mempty st) d) (prop . fromScript)
164+ forAll initialState $ \ st -> forAllMappedDLS st to from fromScript d prop
165+
166+ forAllUniqueDLS
167+ :: (DL. DynLogicModel s , Testable a )
168+ => s
169+ -> DL s ()
170+ -> (Actions s -> a )
171+ -> Property
172+ forAllUniqueDLS st d p =
173+ DL. forAllUniqueScripts st (runDL (Metadata mempty st) d) p
174+
175+ forAllDLS
176+ :: (DL. DynLogicModel s , Testable a )
177+ => s
178+ -> DL s ()
179+ -> (Actions s -> a )
180+ -> Property
181+ forAllDLS st d p =
182+ DL. forAllScripts st (runDL (Metadata mempty st) d) p
183+
184+ forAllMappedDLS
185+ :: (DL. DynLogicModel s , Testable a )
186+ => s
187+ -> (rep -> DL. DynLogicTest s )
188+ -> (DL. DynLogicTest s -> rep )
189+ -> (Actions s -> srep )
190+ -> DL s ()
191+ -> (srep -> a )
192+ -> Property
193+ forAllMappedDLS st to from fromScript d prop =
194+ DL. forAllMappedScripts st to from (runDL (Metadata mempty st) d) (prop . fromScript)
0 commit comments