Hi, if I flatten (from entries.ml
and safe_typing.ml
):
type constant_entry =
| DefinitionEntry : definition_entry -> constant_entry
| ParameterEntry : parameter_entry -> constant_entry
| PrimitiveEntry : primitive_entry -> constant_entry
| SymbolEntry : symbol_entry -> constant_entry
type global_declaration =
| ConstantEntry : Entries.constant_entry -> global_declaration
| OpaqueEntry : unit Entries.opaque_entry -> global_declaration
into only (in entries.ml
)
type constant_entry =
| OpaqueEntry : unit opaque_entry -> constant_entry
| DefinitionEntry : definition_entry -> constant_entry
| ParameterEntry : parameter_entry -> constant_entry
| PrimitiveEntry : primitive_entry -> constant_entry
| SymbolEntry : symbol_entry -> constant_entry
then draw according structure and naming uniformizations from it, especially in add_constant
, do you see objections?
I'm pretty sure this is here for static typing reasons in Safe_typing
I'd advise against trying to merge types and APIs when there is clear use of static invariants expressed in the types.
Some serious time has been passed in making invariants as precise as possible, especially around the kernel API, so please do not disrupt without a clear cut explanation.
Code smells include having to introduce assertions here and there.
There seems indeed to be a play between constant_typing.ml
, which does not set bytecode nor final body, and safe_typing.ml
. Are there particular reasons why constant_typing.ml
does not set them itself?
Constant typing is too low-level, it's only concerned about typing the body
plus there are some tricky horrors related to the with Definition clause for bytecode
once again I've passed unreasonable amounts of time exposing static invariants in there. The Declare layer maybe broken, but at least the kernel is somewhat more rigid.
So, you mean that, somehow, it is rather that the bytecode field should be extracted out of the constant_body
record?
no ?
once again I've passed unreasonable amounts of time exposing static invariants in there
Yes, I'm precisely asking because I see that indeed a lot of care has been taken in ensuring static typing invariants.
why do you want to change it then?
there has been no changes in the kernel that warrant an API change
you should try to bubble up these invariants to Declare, not the other way around
It is about the interaction with declare.ml
being broken. It is about trying to make the structure and motivations for this structure easier to follow.
you should try to bubble up these invariants to Declare, not the other way around
Indeed, I'm trying to make them closer.
it's definitely declare that needs fixing, not the kernel
When you look at add_constant
, the first thing it does it is precisely to split (in two steps) over these 5 entries, with extra ad hoc treatments. Somehow the question is what it would imply to merge the two-step split into one?
I don't know which part of the code you're referring to
in Constant_typing you mean?
As a general rule of thumb, a shorter API is not a better API. There are reason why some signatures take an explicit data rather than an option, this kind of stuff.
In OCaml, defining algebraic types is cheap. Use them to rule out impossible cases statically.
There is a first split in safe_typing.ml and a second in constant_typing.ml.
I wonder what it would imply to inline the case split done in infer_constant in constant_typing.ml inside safe_typing.ml. Would it break invariants?
Secondarily to the question of one-step vs two-steps case split, is it important that the final const_body for opaque is set in safe_typing.ml and not directly in infer_opaque in constant_typing.ml?
For the second point, I think it is indeed relatively important. This separates type-checking per se from other computations about the constant.
OK, I see. So, the idea is really to separate the pure CCI part (in constant_typing.ml) and the non purely CCI part (bytecode and opacity tricks, in safe_typing.ml), right?
Then, flattening the two case splits into one is compatible with this distinction.
Could the handle for opaque entries be the kernel name itself, rather than an object of some abstract type? Any Opaqueproof.opaque
is associated to a unique kernel name, right?
For instance, could Safe_typing.check_opaque
could instead take a kernel name as input?
Such change woud provide a more "logically-minded" model.
IMHO @Hugo Herbelin any change here is moot without a proof of concept of the upper layers taking advantage of it.
Which we don't have at the moment IMO.
What do "upper layers" need? For instance, supporting concurrent constructions of safe environments and, eventually, safe merge of such concurrently-built safe environments be enough?
It is not clear @Hugo Herbelin
I mean, it is hard to know before a fully prototype is assembled
as there are several possible design approaches.
What are you trying to do here?
How do you envision the API being used?
Hugo Herbelin said:
What do "upper layers" need? For instance, supporting concurrent constructions of safe environments and, eventually, safe merge of such concurrently-built safe environments be enough?
That looks pretty complicated to me, what would be such an scenario?
But maybe we can discuss in the call if thing would be easier, or at IRIF
What are you trying to do here?
If you are asking about me, I'm mostly guided these days by simplifying, clarifying, documenting the current code in declare.ml
, with the idea that not only CEP #42 will be easier to implement but the technical debt will diminish, the maintenance will be easier, and the generality of the code will increase.
I did not have in mind "upper layers" a priori and I actually don't know what you are exactly referring to by the words "upper layers" (though I suspect you mean "document managers").
By upper layers indeed I mean whoever is calling that API.
For instance, supporting concurrent constructions of safe environments and, eventually, safe merge of such concurrently-built safe environments be enough?
Isn't it basically what we already provide for the logical part? (But building concurrently the non-logical part might be much more complex.)
Usually the document managers fit this role, but who knows, there are other parts. (For example state handling is both used by the document managers and section mechanism, a design that makes things very complex sometimes)
Regarding the cleanups, I would try to keep the API changes to a minimum, just for a matter of efficiency
My view on this is that changes should be driven by real needs of the users, otherwise they tend to be mostly churn.
But of course it depends.
In the case how of to handle opaque proofs, I think we have no agreed upon plan or satisfying proposal yet, so it makes sense to discuss that first.
In the case how of to handle opaque proofs, I think we have no agreed upon plan or satisfying proposal yet, so it makes sense to discuss that first.
Looks good.
we have no agreed upon plan or satisfying proposal
If we have proposals, we can already compare them!
And we actually already have the current implementation...
Last updated: Oct 13 2024 at 01:02 UTC