Lean: add support for register definitions #894
Conversation
This comment was marked as outdated.
This comment was marked as outdated.
src/lib/state.ml
Outdated
| hardline; | ||
| string " get_"; | ||
| idd; | ||
| colon; |
There was a problem hiding this comment.
Space needed before the colon
src/lib/state.ml
Outdated
| idd; | ||
| colon; | ||
| space; | ||
| string "SailM ("; |
There was a problem hiding this comment.
The brackets for the argument of SailM are not needed because whoever produces a composite term should be in charge of bracketing (in this case doc_typ).
test/lean/reg.expected.lean
Outdated
|
|
||
| open Sail | ||
|
|
||
| class MonadReg where |
There was a problem hiding this comment.
Shouldn't the register state be part of the state that's carried by SailM? That would give us the getter and setter "for free" instead? Or do we want to keep this flexible? What's your opinion on this, @bacam ?
lfrenot
force-pushed
the
lean-register-clean
branch
from
290094b to
6840387
Compare
| | _ -> failwith ("Pattern " ^ string_of_pat_con pat ^ " " ^ string_of_pat pat ^ " not translatable yet.") | ||
|
|
||
| (* Copied from the Coq PP *) | ||
| let rebind_cast_pattern_vars pat typ exp = |
There was a problem hiding this comment.
Does Lean actually need this? (It's to deal with a limitation of Coq's let-binding patterns.)
There was a problem hiding this comment.
Lean can pattern match in let-bindings if there's a single constructor, is that enough?
There was a problem hiding this comment.
That's roughly what Coq allows, except with the limitation that you can't have type annotations deep inside the pattern.
There was a problem hiding this comment.
Oh, now that I think about it, it may also have been to ensure that sufficient bitvector casts are inserted (e.g., when you have bits(8 * 'n) and need bits('n * 8).
| | E_typ (typ, e) -> parens (separate space [doc_exp ctx e; colon; doc_typ ctx typ]) | ||
| | E_typ (typ, e) -> ( | ||
| match e with | ||
| | E_aux (E_assign _, _) -> doc_exp ctx e |
There was a problem hiding this comment.
I might try and get rid of these silly unit type annotations on assignments when they're generated, as they affect several backends.
|
Why not just make the |
@javra that would also be nice, but I'm not sure how make them explicit for PreSailM and implicit for the rest, while still using the variable |
abbrev PreSailM (RegisterType : Register → Type) :=
EStateM Error (@SequentialSate Register RegisterType _ _)I think it should also be explicit in |
|
@javra Thanks, I've done the edits |
Co-authored-by: Jakob von Raumer <[email protected]>
|
Looks good, but maybe some of the commented out code looks old, perhaps those bits should be removed? |
@bacam Yes, thanks for the notice. It should be good now. |
No description provided.