Skip to content

Draft: Abstract state#72

Draft
samuelgruetter wants to merge 3 commits intoAeneasVerif:mainfrom
samuelgruetter:abstract_state
Draft

Draft: Abstract state#72
samuelgruetter wants to merge 3 commits intoAeneasVerif:mainfrom
samuelgruetter:abstract_state

Conversation

@samuelgruetter
Copy link
Copy Markdown

This is my first attempt at sketching how I'd like to abstract over state as proposed in #60.

This code does not compile yet. This PR is meant as a request for early feedback on whether I should continue in this direction.

A few notes:

  • To make sure getters and setters can still use dot notation, I flipped the order of their first (state) and second (destination or register) argument, because the type of the self (first) argument in dot notation cannot be an abstract type.
  • To make sure the execution order is as close as possible to left-to-right, I replaced next newStateExpression by newStateExpression |> next. The pipeline operator is defined in the Lean standard library and I didn't have to add any import or notation-scope-opening to activate it.
  • The StatusFlags record could be removed by using setters for the individual flags, but I kept it because it seems to me that the code tries to defend against accidential omission of a flag, and keeping the StatusFlags record seems to helps towards that goal, but I'm not sure if it's worth keeping these records.
  • Before this PR, all lambdas starting with (λ setcf => ...) invoke setcf twice, so after a beta reduction, the whole body of setcf is duplicated. With this PR, the duplication should be gone, but it now uses a different setter to set specific values than to set an undefined value. I believe it would be best to push the if as far down as possible, all the way into the argument of the setter, like StatusFlag.cf.set (if cond then specificValue else undefinedValue). As far as I can tell, neither the code before this PR nor this PR achieves this. If someone comes up with a solution that achieves this using the Undefined typeclass instead of undefineX methods on StateAccess, I'll be happy to accept this as an indicator that my undefineX methods on StateAccess were a bad idea ;)
  • I don't have strong opinions on argument order, naming, and namespacing. I just picked something that looks reasonable to me and leads to code that gets executed (mostly) from left to right. If/once consensus for abstracting over the state has been reached, I'll be happy to fine-tune argument order and naming etc.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant