I see at least two reasons to declare global fixpoints in one shot:
How would we do that?
A possibility would be to add a new entry MutualDefinitionEntry of mutual_definition_entry
in constant_entry
but the structuration is not exactly the one we want. For instance, we would like the label of the entry to move inside since there would be several labels in the case of mutual definitions. So, this might go with some restructuration of constant_entry
?
We would like the possibility for them to be delayed too.
Maybe would we like also to have mutual definitions of parameters and constants?
Side question: wouldn't it be worth to put OpaqueEntry
at the same level as OpaqueEntry
DefinitionEntry
and ParameterEntry
, e.g. by merging constant_entry
and global_declaration
?
Maybe would we like also to have mutual definitions of parameters and constants?
what does that mean?
I mean something like that, but without losing the body of f
:
Fixpoint f n := match n with 0 => 0 | S n => f n + g n end
with g n {struct n} : nat.
Admitted.
Maybe a bit tortuous though. We would need to distinguish cases according to whether g
depends strictly or largely on f
.
I think you need to change the structure of global environments so that an entry can bind multiple names indeed. If you think ahead how to acommodate inductive-recursive definitions, you probably want something of the shape
type global_env = mutual_declarations list
type mutual_declarations = (kername * declaration) list
type declaration =
| InductiveDecl id
| ConstantDecl cd
This would model something like the mutual
blocks of Agda.
Matthieu Sozeau said:
I think you need to change the structure of global environments so that an entry can bind multiple names indeed.
OK for a change of the structure of global environments at some time, especially if there is some model already in mind, but I was looking at the current time for a light modification which affects only the Safe_typing
API.
I mean something like that, but without losing the body of f:
but g cannot depend on f so we can just declare it as an axiom first
Gaëtan Gilbert said:
I mean something like that, but without losing the body of f:
but g cannot depend on f so we can just declare it as an axiom first
Yes, let's forget about it. (Maybe with recursive-recursive types where f
occurs in the type of g
, but let's forget also.)
I was typically thinking at an extension of Safe_typing
like:
val add_fixpoint : fixpoint_entry -> safe_environment -> safe_environment
val add_cofixpoint : cofixpoint_entry -> safe_environment -> safe_environment
with
type fixpoint_entry = {
fixpoint_entry_prefix : rel_context;
fixpoint_entry_secctx : Id.Set.t;
fixpoint_entry_names : Id.t array;
fixpoint_entry_bodies : constr array;
fixpoint_entry_types : types array;
fixpoint_entry_types : universe_entry;
fixpoint_entry_opaque : bool;
or to add a FixpointEntry
to add_constant
.
Then, the effect on the environment would have been the same (except for constants referring to themselves). Ready to consider alternatives which would eventually help induction-recursion though.
Last updated: Oct 13 2024 at 01:02 UTC