stefan-hoeck / idris2-hedgehog

An Idris port of the Haskell Hedghog library
BSD 2-Clause "Simplified" License
32 stars 3 forks source link

[ refactor ] Change runners to be runnable in pure or purified context #37

Closed buzden closed 1 year ago

buzden commented 1 year ago

The third solution of a problem discussed in #36

buzden commented 1 year ago

Oh, now reading through the comments in #36, I see that you've changed the style of signatures. In this module I used the style that was already in that module. I think, changing the style should be separate from the proposed change for the future traceability

stefan-hoeck commented 1 year ago

I'm afraid I don't understand how and why this solves the issue discussed in #36. Please add documentation / explanations both to the code and to this PR.

buzden commented 1 year ago

I'm afraid I don't understand how and why this solves the issue discussed in #36. Please add documentation / explanations both to the code and to this PR.

Newly added interfaces now allow to run hedgehog in a pure environment with an ability to analyse the printed output of its checks. I added a little bit of documentation to the interfaces themselves, but more importantly, I added a testing facility which I talked about in the third variant in #36. It tests behaviour of hedgehog itself (including shrinking) both when testing succeeds and fails, an all that is inside hedgehog properties. You can look at the last commit that adds those.

buzden commented 1 year ago

@stefan-hoeck Are my explanations and added tests understandable enough?

stefan-hoeck commented 1 year ago

Thank you very much for this. I'm going to merge as it is. Please rebase #36 if necessary. Afterwards, I'll have another look at that one.