| Age | Commit message (Collapse) | Author |
|---|
|
|
|
vernac/
Ack-by: Janno
Reviewed-by: SkySkimmer
|
|
This is useful to remove some duplicate bits in other declare files.
|
|
The code is self-contained and only used by commands; this also
highlights the several `Libobject.obj` registered for each
declaration.
|
|
|
|
|
|
|
|
The general idea is to move tests on scope=Discharge and on
Lib.sections_are_opened up in the call stack. This allows better
control over the universe manipulation.
There are some corner case behaviour change, eg:
- [Context (foo:=bla)] outside a section correctly declares an
axiom (fix #10668)
- (not observable) universes for [Variable A B : Type] in section are declared only once
- universes and universe names for [Axiom A B : Type] are declared
only once. This changes the qualification of the universe name:
before it was the last axiom (so [B.u0]), now it's the first
one ([A.u0]).
Probably nobody cares about this.
- context outside section uses different [kind]
I'm not sure why context outside a section behaves differently based
on whether we're in a module type, I tried to preserve it but maybe we
should uniformize.
The universe manipulation for Axiom (in the declare_assumptions
function) is a bit awkward, maybe when there are multiple monomorphic
axioms instead of trying to attach the universes to the first one we
should just declare them separately like with Context. OTOH unlike
with context dropping the universe names seems incorrect.
|
|
Primitives don't have anything to do with assumptions.
|
|
(letins still declare universes in declare_variable as they use
entries)
The section check_same_poly is moved to declare_universe_context (it
makes more sense there, universe polymorphism doesn't apply to the
variables/letins themselves)
|
|
|
|
This lets us remove the passing around of "status" in comassumption
and generally makes highlighting axiom adding lines in coqide more
reliable as there's no need for per-command code.
If a command adds multiple axioms it will emit AddedAxiom multiple
times, this doesn't seem to be a problem though.
We may wonder if "Fail Fail Axiom" should be highlighted as
"Axiom" (both before and after this commit it is).
|
|
Not pretty, but it had to be done some day, as `Globnames` seems to be
on the way out.
I have taken the opportunity to reduce the number of `open` in the
codebase.
The qualified style would indeed allow us to use a bit nicer names
`GlobRef.Inductive` instead of `IndRef`, etc... once we have the
tooling to do large-scale refactoring that could be tried.
|
|
|
|
The object was mostly for wrangling universes, but we already have the
universe object for that.
It's also used by some code which iterates over objects to find
variables.
Search used to do this but was changed in a previous commit.
Prettyp.print_context and derivatives do this and I don't understand
it enough to fix it, so I kept a dummy object around. It seems like a
not very common used Print family (not documented AFAICT) so maybe we
should remove it all instead.
|
|
They are clearly not at the same importance level, thus we use a named
parameter and isolate the kinds as to allow further improvements and
refactoring.
|
|
We move the bulk of `Decl_kinds` to a better place [namely
`interp/decls`] and refactor the use of this information quite a bit.
The information seems to be used almost only for `Dumpglob`, so it
certainly should end there to achieve a cleaner core.
Note the previous commits, as well as the annotations regarding the
dubious use of the "variable" data managed by the `Decls` file.
IMO this needs more work, but this should be a good start.
|
|
It was never used actually.
|
|
Followup on "[api] Remove `polymorphic` type alias, use labels instead."
|
|
This is more in-line with attributes and the rest of the API, and
makes some code significantly clearer (as in `foo true false false`,
etc...)
|
|
This datatype does belong to this layer.
|
|
We split `{goal,declaration,assumption}_kind` into their
components. This makes sense as each part of this triple is handled by
a different layer, namely:
- `polymorphic` status: necessary for the lower engine layers;
- `locality`: only used in `vernac` top-level constants
- `kind`: merely used for cosmetic purposes [could indeed be removed /
pushed upwards]
We also profit from this refactoring to add some named parameters to
the top-level definition API which is quite parameter-hungry.
More refactoring is possible and will come in further commits, in
particular this is a step towards unifying the definition / lemma save path.
|
|
This allows to desynchronize the kernel-facing API from the proof-facing one.
|
|
|
|
|
|
|
|
Formerly, knowing if a declaration was to be discharged, to be global
but invisible at import, or to be global but visible at import was
obtained by combining the parser-level information (i.e. use of
Variable/Hypothesis/Let vs use of Axiom/Parameter/Definition/..., use
of Local vs Global) with the result of testing whether there were open
sections.
We change the meaning of the Discharge flag: it does not tell anymore
that it was syntactically a Variable/Hypothesis/Let, but tells the
expected semantics of the declaration (issuing a warning in the
parser-to-interpreter step if the semantics is not the one suggested
by the syntax). In particular, the interpretation/command engine
becomes independent of the parser.
The new "semantic" type is:
type import_status = ImportDefaultBehavior | ImportNeedQualified
type locality = Discharge | Global of import_status
In the process, we found a couple of inconsistencies in the treatment
of the locality status. See bug #8722 and test file LocalDefinition.v.
|
|
This is to avoid depending on the combination "Discharge" + no opened
section to trigger an automatic declaration of instance.
|
|
|
|
This lets us avoid passing ~ontop to do_definition and co, and after #10050
to even more functions.
|
|
This code was originally part of #8811, authored by Gaëtan Gilbert.
It seems we are not very consistent on what we do when we use
`ParameterEntry`, specially w.r.t. universes but as code cleanup
progresses we will have a better view.
Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
|
|
I had to reorganize the code a bit. The Context command moved to
comAssumption, as it is not so related to type classes. We were able to
remove a few hooks on the way.
|
|
Not sure the warning is worth the extra parameter.
|
|
|
|
Kernel should be mostly correct, higher levels do random stuff at
times.
|
|
|
|
Reviewed-by: vbgl
|
|
I think the usage looks cleaner this way.
|
|
"registered" sounds like it existed before the command.
This could use assumption_message which is currently the same, but I
don't think it has the right semantic.
|
|
We remove all calls to `Flags.is_program_mode` except one (to compute
the default value of the attribute). Everything else is passed
explicitely, and we remove the special logic in the interpretation loop
to set/unset the flag.
This is especially important since the value of the flag has an impact on
proof modes, so on the separation of parsing and execution phases.
|
|
This work makes it possible to take advantage of a compact
representation for integers in the entire system, as opposed to only
in some reduction machines. It is useful for heavily computational
applications, where even constructing terms is not possible without such
a representation.
Concretely, it replaces part of the retroknowledge machinery with
a primitive construction for integers in terms, and introduces a kind of
FFI which maps constants to operators (on integers). Properties of these
operators are expressed as explicit axioms, whereas they were hidden in
the retroknowledge-based approach.
This has been presented at the Coq workshop and some Coq Working Groups,
and has been used by various groups for STM trace checking,
computational analysis, etc.
Contributions by Guillaume Bertholon and Pierre Roux <Pierre.Roux@onera.fr>
Co-authored-by: Benjamin Grégoire <Benjamin.Gregoire@inria.fr>
Co-authored-by: Vincent Laporte <Vincent.Laporte@fondation-inria.fr>
|
|
write_function
|
|
optional.
|
|
|
|
People should use Declare Instance instead.
|
|
(same for solve_remaining_evars)
This is the standard way to use these functions, with 1 exception in
Unification.
|
|
|
|
It's basically an occur check so it makes sense to put it in vars
|
|
|
|
|
