-
Notifications
You must be signed in to change notification settings - Fork 675
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Stronger invariants in the structure of Declare.proof_entry #19237
Stronger invariants in the structure of Declare.proof_entry #19237
Conversation
let force_entry_body entry = | ||
match entry.proof_entry_body with | ||
| Default { body; opaque } -> body, opaque | ||
| DeferredOpaque { body; feedback_id = Some _ } -> CErrors.anomaly (str "Forcing a proof with feedback") |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I think you should enforce this statically, since several callers below are using Future.from_val
for no good reason.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
It remains 3 Future.from_val
in the current PR:
- one is to use
cast_opaque_proof_entry
and we could have a third case to it to avoid the from_val, - one is to declare an opaque
Let
: I don't understand well the code but it can probably be avoided, - the third one is to declare deferred univs for a non-deferred constant, and this could be avoided too.
So, all three could be avoided (assuming you are ok to have a third variant of cast_opaque_proof_entry
).
Regarding force_entry_body
, this is used for obligations and for Derive
. I have the feeling that we rely here on stm invariants, that is that the stm will not defer proofs of obligations and proofs of Derive
. I don't know how to ensure that (except by duplicating or annotating the type proof_object
so that close_proof
and close_future_proof
have different return types). In any cases, it would modify the API of declare.ml
and I'm not very comfortable at doing it now, at least until the whole coq/rfcs#89 is in place.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
third variant of cast_opaque_proof_entry
GADTs can do wonder to prevent code duplication.
I'm not very comfortable at doing it now
No problem, it's better to do it incrementally.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
If one wants to avoid futures as much as possible, one would also need a version of Opaque.declare_defined_opaque
that takes a non deferred body. Do you want that?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
...or a dependently-typed version of Opaque.declare_defined_opaque
.
4ebee40
to
2021c18
Compare
@coqbot run full ci |
@coqbot run full ci |
In particular: - cast_entry_proof - cast_opaque_entry_proof - declare_private_constant - build_constant_by_tactic etc., have finer types
2021c18
to
d05a2c1
Compare
@ppedrot are you assigning? |
I think I had a merge conflict with master when trying to run this locally after the merge of another declare cleanup PR. Let's just @coqbot run full ci just in case |
@coqbot merge now |
The PR enforces stronger invariants in the different uses of
proof_entry
.Using a sum type
Default
(Transparent
|Opaque
)|DeferredOpaque
, the typeproof_entry
is morally divided into the following variants:constr pproof_entry
: no side effect, no local universes, not deferred'eff default_proof_body pproof_entry
, parameterized by effects: not deferred, possibly transparent, possibly with local universes'eff proof_entry
, parameterized by effects, the most general: possibly deferred, possibly transparent, possibly with local universesThe following excerpt of functions have then refined types:
cast_entry_proof
cast_opaque_entry_proof
declare_private_constant
build_constant_by_tactic
Together with a forthcoming PR which will merge
close_proof
andclose_proof_delayed
around a typeImmediate(body,typ,uctx)
|Delayed(body,type,uctx)
, we should be able to make progresses in the direction of coq/rfcs#89, that is to have bothclose_proof
and immediate definitions producing anImmediate
|Delayed
which is then turned into aDefault
(Transparent
|Opaque
)|DeferredOpaque
proof entry, then processed bydeclare_entry
(to distinguish between in or outside a section) and finally bydeclare_constant
.The main commit is the 2nd one. The 3rd commit is mostly about the structuration of the code.