search

tweag / cooked-validators

MIT License
39 stars 11 forks source link

Mm/ltl tests maybe #135

Closed mmontin closed 2 years ago

mmontin commented 2 years ago

This PR aims at extending Carl's example on usage of modifications. This idea is to factor modifications to type a -> m a where a is a monad. This PR also adds the notion of label where a modification stamps a value that has been modified, otherwise there were no way to actually know if a certain modification was applied. This PR assembles two example files, one using the identity monad, and the other the maybe monad. This idea would be to use the example to maybe slightly extend what is provided to the users (the type of modifications for instance) and possibly use it for modifications going from a to List a where a single modification can yield several outcomes. This could help clarify such semantics.

mmontin commented 2 years ago

I believe this one is completely outdated, can you confirm @carlhammann ?

carlhammann commented 2 years ago

I believe this one is completely outdated, can you confirm @carlhammann ?

Yes, it is, insofar as it is based on a version of cooked that has the single-transaction attack type defined as TxSkel -> Maybe TxSkel, and cooked has evolved quite a bit...

As long as we still keep the (very valid) ideas in this PR in our heads, I think we schould close it.

carlhammann commented 2 years ago

As per my last comment, I'll close this now.