Guillaume Melquiond (Mar 01 2022 at 15:07): Guillaume Melquiond (Mar 01 2022 at 15:07):I am trying to implement opaque constants (something akin to Lemma foo := bar.) and I am a bit confused by the code in Declare. I don't understand if this can be performed with one of the existing constructors (i.e., ConstantEntry and OpaqueEntry) or if I need a third case.
Emilio Jesús Gallego Arias (Mar 01 2022 at 15:11):It should work with the existing ones
Guillaume Melquiond (Mar 01 2022 at 15:13):So, which one?
Emilio Jesús Gallego Arias (Mar 01 2022 at 15:23):Doesn't Declare.declare_definition ~opaque:true do what you want?
Guillaume Melquiond (Mar 01 2022 at 15:27):No, it dies on the assert false in Declare.cast_opaque_proof_entry.
Guillaume Melquiond (Mar 01 2022 at 15:38):One of the things I don't understand is why proof_entry_type is an option and when it stops being None. (It has to stop at some point, right? Because every entry has a type, doesn't it?)
Emilio Jesús Gallego Arias (Mar 01 2022 at 15:40):I think in some cases it was inferred
Emilio Jesús Gallego Arias (Mar 01 2022 at 15:40):But that code is indeed quite tricky let's wait for @Pierre-Marie Pédrot who is the cast wizard
Guillaume Melquiond (Mar 01 2022 at 15:41):When doing Definition foo := bar, proof_entry_type is None. So, when I transpose the code to Lemma foo := bar, the assertion fails because it is still None. And I don't understand when it is supposed to stop being None for Definition foo := bar.
Emilio Jesús Gallego Arias (Mar 01 2022 at 15:42):Ok, I think I remember now.
Emilio Jesús Gallego Arias (Mar 01 2022 at 15:42):For opaque proof entries, the kernel is not allowed to look into the term
Emilio Jesús Gallego Arias (Mar 01 2022 at 15:42):as it could be delayed, so providing the type is mandatory
Emilio Jesús Gallego Arias (Mar 01 2022 at 15:43):So the current API disallows #[opaque] Definition foo := bar. as-is
Emilio Jesús Gallego Arias (Mar 01 2022 at 15:43):I don't know if that makes sense, but it is what it is
Emilio Jesús Gallego Arias (Mar 01 2022 at 15:45):Note that the kernel accepts that due to the type of Entries.type definition_entry
Emilio Jesús Gallego Arias (Mar 01 2022 at 15:46):I mean, it allows for the type to be absent, but not in the case there may not a body
Emilio Jesús Gallego Arias (Mar 01 2022 at 15:46):@Guillaume Melquiond does it make sense?
Emilio Jesús Gallego Arias (Mar 01 2022 at 15:48):That's really due to the way the kernel API is
Emilio Jesús Gallego Arias (Mar 01 2022 at 15:48):I'm sure it can be improved
Guillaume Melquiond (Mar 01 2022 at 15:48):Sure, I understand why the type is mandatory for opaque entries. But I don't understand how the code can get away with transparent entries not having a type.
Emilio Jesús Gallego Arias (Mar 01 2022 at 15:54):The kernel doesn't require it, and will infer the type
Emilio Jesús Gallego Arias (Mar 01 2022 at 15:54):See Entries.definition_entry that's a kernel API
Emilio Jesús Gallego Arias (Mar 01 2022 at 15:54):type definition_entry = {
const_entry_body : constr;
(* List of section variables *)
const_entry_secctx : Id.Set.t option;
const_entry_type : types option;
const_entry_universes : universes_entry;
const_entry_inline_code : bool;
}
however, in this case, the body is mandatory
Guillaume Melquiond (Mar 01 2022 at 15:56):But, when you do About foo, the kernel does not infer the type on the fly, does it? So, the type is already there somewhere. But I don't understand where.
Emilio Jesús Gallego Arias (Mar 01 2022 at 15:57):yes, Entries.definition_entry is the _input_ to the kernel
Emilio Jesús Gallego Arias (Mar 01 2022 at 15:57):the kernel will infer the type and store it
Emilio Jesús Gallego Arias (Mar 01 2022 at 15:57):yes it does infer it on the fly, _when_ declaring the constant
Emilio Jesús Gallego Arias (Mar 01 2022 at 15:57):or if you specify the type, the kernel will infer, and compare with the provided one
Emilio Jesús Gallego Arias (Mar 01 2022 at 15:57):that's how the kernel works basically I understand
Emilio Jesús Gallego Arias (Mar 01 2022 at 15:58):it doesn't implement bi-directional TC
Emilio Jesús Gallego Arias (Mar 01 2022 at 15:58):the type is stored in the environment
Emilio Jesús Gallego Arias (Mar 01 2022 at 15:58):Declarations.pconstant_body
Emilio Jesús Gallego Arias (Mar 01 2022 at 15:59):It took me a while to realize which types are input and what types are output
Emilio Jesús Gallego Arias (Mar 01 2022 at 15:59):I'm sure we could improve the terminology here
Emilio Jesús Gallego Arias (Mar 01 2022 at 15:59):tho once you know it, kind of makes sense
Emilio Jesús Gallego Arias (Mar 01 2022 at 15:59):I guess
Emilio Jesús Gallego Arias (Mar 01 2022 at 16:01):Does it make sense @Guillaume Melquiond ?
Guillaume Melquiond (Mar 01 2022 at 16:04):Yes. But what about my original question? Can it be done with one of the two existing constructors or do I need to add a third one?
Guillaume Melquiond (Mar 01 2022 at 16:05):I see that the kernel has Safe_typing.translate_direct_opaque. So, the kernel actually already supports Lemma foo := bar. I just need a way to invoke it.
Emilio Jesús Gallego Arias (Mar 01 2022 at 16:10):I would try to avoid adding a new constructor
Emilio Jesús Gallego Arias (Mar 01 2022 at 16:10):but I'm not sure if it can be done
Pierre-Marie Pédrot (Mar 01 2022 at 16:12):Don't use translate_direct_opaque, this is side-effect specific stuff
Emilio Jesús Gallego Arias (Mar 01 2022 at 16:12):That's internal actually, I got confused because I thought you were talking about Declare, but you are actually talking about the constructors in Safe_typing
Pierre-Marie Pédrot (Mar 01 2022 at 16:13):use the Declare primitives to infer the type of the opaque definition, and send that to the kernel
Pierre-Marie Pédrot (Mar 01 2022 at 16:13):the kernel should treat any opaque stuff as an axiom
Pierre-Marie Pédrot (Mar 01 2022 at 16:14):there is a bit of unfortunate coupling between the various entries
Guillaume Melquiond (Mar 01 2022 at 16:21):Pierre-Marie Pédrot said:
use the Declare primitives to infer the type of the opaque definition, and send that to the kernel
Do you have something specific in mind? Because I have been staring at Declare for two weeks now and I don't see anything that could help here.
Emilio Jesús Gallego Arias (Mar 01 2022 at 16:38):Declare does not indeed infer types
Emilio Jesús Gallego Arias (Mar 01 2022 at 16:38):some examples of code doing that may be in vernac
Gaëtan Gilbert (Mar 01 2022 at 20:14):in https://github.com/coq/coq/blob/aa0d53369c40ceab7a31e7a1abf602efc7f00bc2/vernac/comDefinition.ml#L99-L100 when it's opaque call interp_constr_evars_impls_ty (you will need to add this function, behaving as interp_constr_evars_impls but also returning the type, kinda annoying to do as all the Constrintern.interp_* functions use Pretyping.understand_* variants that drop the type instead of eg understand_tcc_ty which returns it, but shouldn't be difficult)
NB only when it's opaque as giving the type to the kernel has perf cost so shouldn't be done when not needed
Last updated: Dec 05 2023 at 05:01 UTC