Interactive mode to complete instances in tactics mode#595
Interactive mode to complete instances in tactics mode#595cecilemarcon wants to merge 16 commits into
Conversation
|
Quick thing, if the test needs the Stdlib, it should go into tests_stdlib |
| func under term, list (pair term term) -> term. | ||
| under (fun N Ty F) Acc (fun N Ty F') :- | ||
| @pi-decl N Ty x\ | ||
| under (F x) [(pr x Ty)|Acc] (F' x). | ||
| under (app L) Acc (app L') :- | ||
| aux Acc L L'. | ||
|
|
||
| func aux list (pair term term), list term -> list term. | ||
| aux _ [] []. | ||
| aux Acc [T|TS] [T|TS'] :- | ||
| coq.typecheck T Ty ok, | ||
| coq.typecheck Ty TyTy ok, | ||
| %coq.typecheck-ty does not make coercions | ||
| (not (TyTy = {{Prop}}); T = global _), !, | ||
| aux Acc TS TS'. | ||
| aux Acc [T|TS] [T'|TS'] :- | ||
| std.spy! (abstract Acc T TA), | ||
| log.coq.env.add-const _ TA _ @opaque! C, | ||
| T' = app [(global (const C))|{std.map Acc fst}], | ||
| aux Acc TS TS'. | ||
|
|
||
| func abstract list (pair term term), term -> term. | ||
| abstract [] T T' :- | ||
| copy T T'. | ||
| abstract [(pr V Ty) | A] T (fun `x` Ty F) :- | ||
| pi w\ (copy V w :- !) => abstract A T (F w). | ||
|
|
There was a problem hiding this comment.
I think this code should go to utils, maybe in a namespace abstract-props-as-lemmas.
You can then leave here just the call to abstract-props-as-lemmas.main (now called under).
Related design question for @CohenCyril is how configurable this should be, i.e. instead of using Prop as a marker one may want to flag the fields of mixins/factories as not-data. It may be possible to have a default (Prop) and a field-attribute as https://rocq-prover.org/doc/master/refman/language/extensions/canonical.html#rocq:attr.canonical (in rocq/Elpi) but it may require some little work.
There was a problem hiding this comment.
Yes I think it is better if configurable. But reasonable choices are essentially Prop, SProp and hProp. So possibly just registering them (as a open list) and unifying with them is enough.
There was a problem hiding this comment.
An issue with moving that code to utils is that it uses "log.coq.env.add-const" which is in log and which in turns uses some code from utils (eg "avoid-name-collision)
I could always create a new file to store these functions...
There was a problem hiding this comment.
Ignore log, the log module is a relic. I guess the collision avoidance code can go to utils as well.
| coq.typecheck T Ty ok, | ||
| coq.typecheck Ty TyTy ok, | ||
| %coq.typecheck-ty does not make coercions | ||
| (not (TyTy = {{Prop}}); T = global _), !, |
There was a problem hiding this comment.
if T is globla_ we don't really need to typecheck it. You could have a "fast path" for this case.
like a rule axu Acc [global _ as T|....
| func under term, list (pair term term) -> term. | ||
| under (fun N Ty F) Acc (fun N Ty F') :- | ||
| @pi-decl N Ty x\ | ||
| under (F x) [(pr x Ty)|Acc] (F' x). |
There was a problem hiding this comment.
It may make sense to have a triple here and also store N, and use that N in abstract in place of `x`
There was a problem hiding this comment.
yes, done ! the name of the parameter is used in the abstraction
| }}. | ||
|
|
||
| #[proof="end"] | ||
| Elpi Export HB.endinstance. |
3 participants
This adds an [#[interactive]] attribute to the HB.instance command.
This attribute opens goals to complete to finish the instance declaration.
Once these goals are completed, one uses the HB.endinstance command to finish the instance.
Any suggestions welcome !