[do not merge] semantics-refactor #14
Conversation
| Fixpoint eval_expr(st: state)(e: expr): option (word wXLEN) := | ||
| Set Universe Polymorphism. | ||
| Unset Universe Minimization ToSet. | ||
| (* TODO: should we do this? |
There was a problem hiding this comment.
what do these two lines do, and why do you need it?
There was a problem hiding this comment.
Non-universe-polymorphic definitions are depraceted, we use polymorphic ones. Universe Minimization ToSet is a backwards compatability mode for that.
Primitive Projections means that you never need to destruct records to get something to typecheck.
| | Some x => f | ||
| | None => None | ||
| end) | ||
| (right associativity, at level 60, x pattern). |
There was a problem hiding this comment.
Why is this a local notation? Couldn't you put this into a library file?
There was a problem hiding this comment.
We could, but I don't want to have the readers of the semantics guessing what <- means in this particular context.
| Local Notation interp_cont := Imp.(_interp_cont). | ||
|
|
||
| (* TODO: record ImpParametersOK *) | ||
| Context {mword_eq_dec : DecidableRel (@eq (Imp.varname p))}. |
There was a problem hiding this comment.
Why would you separate ImpParameters and ImpParametersOk?
Why don't you use DecidableEq?
There was a problem hiding this comment.
Separete to allow for parallel compilation of proofs (and in other use cases, reification of the code that doesn't have proofs in it).
| end. | ||
|
|
||
| Context {set_varname: Type}. | ||
| Context {varset: set set_varname varname}. |
There was a problem hiding this comment.
Should these two go into ImpParameters too?
There was a problem hiding this comment.
No, it is not necessary for defining the semantics of the language.
| Record ImpParameters := | ||
| { | ||
| mword : Type; | ||
| mword_nonzero : mword -> bool; |
There was a problem hiding this comment.
abstracting over the word type to hide the dependent type is nice, I meant to do this for a while already
| Local Inductive cont : Type := | ||
| | CSuspended(_:T) | ||
| | CSeq(s1:cont) (s2: stmt) | ||
| | CStack(st: varmap)(c: cont)(binds rets: list varname). |
There was a problem hiding this comment.
What's the meaning of these 3 cases?
How much do we commit to by putting this into the semantics?
There was a problem hiding this comment.
This is in the refactor PR by accident, let's discuss it separately from the actual refactor.
|
|
||
| Section WithFunctions. | ||
| Context (lookupFunction : funname -> option (list varname * list varname * stmt)). | ||
| Local Fixpoint interp_stmt(f: nat)(st: varmap)(m: mem)(s: stmt): option (varmap*mem*option(cont ioact)) := |
There was a problem hiding this comment.
Is there a way to instantiate ioact with something "empty" such that the existing proofs will still go through?
| _interp_stmt : forall (lookupFunction : funname -> option (list varname * list varname * stmt))(f: nat)(st: varmap)(m: mem)(s: stmt), option (varmap*mem*option(cont ioact)); | ||
| _interp_cont : forall (lookupFunction : funname -> option (list varname * list varname * stmt))(f: nat)(st: varmap)(m: mem)(s: cont ioret), option (varmap*mem*option(cont ioact)); | ||
| }. | ||
| Definition Imp : ImpType := Build_ImpType expr stmt cont interp_expr interp_stmt interp_cont. |
There was a problem hiding this comment.
yet another level of wrapping and indirection 😉 -- why is this needed?
There was a problem hiding this comment.
No indirection here, just exporting. In Ocaml this would be in an mli file.
There was a problem hiding this comment.
Actually, it is more than exporting. Not making a record of these definitions would mean that the parameters record would be duplicated for each definition in Imp. I think https://people.csail.mit.edu/jgross/personal-website/papers/category-coq-experience-itp-submission.pdf explains how that results in sadness and slowness.
| Imp.varmap_operations := p.(varmap_operations); | ||
| |}. | ||
| Definition RISCVImp (p:RISCVImpParameters) : Imp.ImpType (ImpParameters_of_RISCVImpParameters p) | ||
| := Imp.Imp (ImpParameters_of_RISCVImpParameters p). |
There was a problem hiding this comment.
By making the right typeclass instances into available, you'd get this for free...
| ] in | ||
| fun bw varname funnname actname varmap varmap_operations => | ||
| RISCVImp (Build_RISCVImpParameters bw varname funnname actname varmap varmap_operations). | ||
| *) |
There was a problem hiding this comment.
This looks suspicious, I guess you'll need it at some point... Will you have to do this to make sure "rewrite" finds matching terms? And is there a risk that the typechecker isn't happy unless you destruct a parameters record?
There was a problem hiding this comment.
We won't need it, it was just a test. If record destruction would become an issue we could just turn on primitive projections for that record.
| { set_solver. } | ||
| { set_solver. } | ||
| { apply singleton_set_spec in H. auto. } | ||
| { apply union_spec in H. |
There was a problem hiding this comment.
Just curious, why do you prefer { over bullets?
There was a problem hiding this comment.
because brackets for one goal do not force the choice of delimiters for other goals. Here I can write 1,2: in the last case.
|
I am not happy with the boilerplate either. But what else would we do? Using the module system would have less boilerplate but the boilerplate would be more arcane; using typeclasses breaks typechecking errors and this type-driven development in most cases where I have seen it used, and often tactics end up being sensitive to syntactic details of typeclass inference output (I had to change some tactics here because of that). |
|
Full version with desugaring of modules into records at source level: https://github.com/mit-plv/bedrock2/tree/refactor-even-more-boilerplate |
|
The remaining boilerplate could be removed using these two changes:
If both are applied, we get https://github.com/mit-plv/bedrock2/tree/typeclasses-without-functors |
creating a PR, hoping that it will let me comment on several commits at a time...