Stream: Coq devs & plugin devs

Topic: Opaque constants


view this post on Zulip 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.

view this post on Zulip Emilio Jesús Gallego Arias (Mar 01 2022 at 15:11):

It should work with the existing ones

view this post on Zulip Guillaume Melquiond (Mar 01 2022 at 15:13):

So, which one?

view this post on Zulip Emilio Jesús Gallego Arias (Mar 01 2022 at 15:23):

Doesn't Declare.declare_definition ~opaque:true do what you want?

view this post on Zulip Guillaume Melquiond (Mar 01 2022 at 15:27):

No, it dies on the assert false in Declare.cast_opaque_proof_entry.

view this post on Zulip 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?)

view this post on Zulip Emilio Jesús Gallego Arias (Mar 01 2022 at 15:40):

I think in some cases it was inferred

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Emilio Jesús Gallego Arias (Mar 01 2022 at 15:42):

Ok, I think I remember now.

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 01 2022 at 15:42):

as it could be delayed, so providing the type is mandatory

view this post on Zulip Emilio Jesús Gallego Arias (Mar 01 2022 at 15:43):

So the current API disallows #[opaque] Definition foo := bar. as-is

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 01 2022 at 15:46):

@Guillaume Melquiond does it make sense?

view this post on Zulip Emilio Jesús Gallego Arias (Mar 01 2022 at 15:48):

That's really due to the way the kernel API is

view this post on Zulip Emilio Jesús Gallego Arias (Mar 01 2022 at 15:48):

I'm sure it can be improved

view this post on Zulip 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.

view this post on Zulip Emilio Jesús Gallego Arias (Mar 01 2022 at 15:54):

The kernel doesn't require it, and will infer the type

view this post on Zulip Emilio Jesús Gallego Arias (Mar 01 2022 at 15:54):

See Entries.definition_entry that's a kernel API

view this post on Zulip 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;
}

view this post on Zulip Emilio Jesús Gallego Arias (Mar 01 2022 at 15:55):

however, in this case, the body is mandatory

view this post on Zulip 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.

view this post on Zulip Emilio Jesús Gallego Arias (Mar 01 2022 at 15:57):

yes, Entries.definition_entry is the _input_ to the kernel

view this post on Zulip Emilio Jesús Gallego Arias (Mar 01 2022 at 15:57):

the kernel will infer the type and store it

view this post on Zulip Emilio Jesús Gallego Arias (Mar 01 2022 at 15:57):

yes it does infer it on the fly, _when_ declaring the constant

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 01 2022 at 15:57):

that's how the kernel works basically I understand

view this post on Zulip Emilio Jesús Gallego Arias (Mar 01 2022 at 15:58):

it doesn't implement bi-directional TC

view this post on Zulip Emilio Jesús Gallego Arias (Mar 01 2022 at 15:58):

the type is stored in the environment

view this post on Zulip Emilio Jesús Gallego Arias (Mar 01 2022 at 15:58):

Declarations.pconstant_body

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 01 2022 at 15:59):

I'm sure we could improve the terminology here

view this post on Zulip Emilio Jesús Gallego Arias (Mar 01 2022 at 15:59):

tho once you know it, kind of makes sense

view this post on Zulip Emilio Jesús Gallego Arias (Mar 01 2022 at 15:59):

I guess

view this post on Zulip Emilio Jesús Gallego Arias (Mar 01 2022 at 16:01):

Does it make sense @Guillaume Melquiond ?

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Emilio Jesús Gallego Arias (Mar 01 2022 at 16:10):

I would try to avoid adding a new constructor

view this post on Zulip Emilio Jesús Gallego Arias (Mar 01 2022 at 16:10):

but I'm not sure if it can be done

view this post on Zulip Pierre-Marie Pédrot (Mar 01 2022 at 16:12):

Don't use translate_direct_opaque, this is side-effect specific stuff

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Pierre-Marie Pédrot (Mar 01 2022 at 16:13):

the kernel should treat any opaque stuff as an axiom

view this post on Zulip Pierre-Marie Pédrot (Mar 01 2022 at 16:14):

there is a bit of unfortunate coupling between the various entries

view this post on Zulip 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.

view this post on Zulip Emilio Jesús Gallego Arias (Mar 01 2022 at 16:38):

Declare does not indeed infer types

view this post on Zulip Emilio Jesús Gallego Arias (Mar 01 2022 at 16:38):

some examples of code doing that may be in vernac

view this post on Zulip 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: Feb 06 2023 at 18:03 UTC