| Age | Commit message (Collapse) | Author |
|---|
|
We move the role data into the evarmap instead.
|
|
We rename modify to map [more in line with the rest of the system] and
make the endline function specific, as it is only used in one case.
|
|
The main idea of this PR is to distinguish the types of "proof object"
`Proof_global.t` and the type of "proof object associated to a
constant, the new `Lemmas.t`.
This way, we can move the terminator setup to the higher layer in
`vernac`, which is the one that really knows about constants, paving
the way for further simplification and in particular for a unified
handling of constant saving by removal of the control inversion here.
Terminators are now internal to `Lemmas`, as it is the only part of
the code applying them.
As a consequence, proof nesting is now handled by `Lemmas`, and
`Proof_global.t` is just a single `Proof.t` plus some environmental
meta-data.
We are also enable considerable simplification in a future PR, as this
patch makes `Proof.t` and `Proof_global.t` essentially the same, so we
should expect to handle them under a unified interface.
|
|
Reviewed-by: aspiwack
Ack-by: ejgallego
Reviewed-by: ppedrot
|
|
Ack-by: SkySkimmer
Reviewed-by: ppedrot
|
|
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.
|
|
|
|
|
|
Typically instead of [start_proof : ontop:Proof_global.t option -> bla ->
Proof_global.t] we have [start_proof : bla -> Proof_global.pstate] and
the pstate is pushed on the stack by a caller around the
vernacentries/mlg level.
Naming can be a bit awkward, hopefully it can be improved (maybe in a
followup PR).
We can see some patterns appear waiting for nicer combinators, eg in
mlg we often only want to work with the current proof, not the stack.
Behaviour should be similar modulo bugs, let's see what CI says.
|
|
We remove unused parts of the API, almost all of them belonging to the
legacy engine. This was detected using coverage testing.
The list is provisional and should be subject to change, let's see
what CI says.
|
|
We get rid of the future wrappers, as all callers are immediately forcing
the result.
|
|
|
|
|
|
Reviewed-by: SkySkimmer
Ack-by: gares
|
|
Ack-by: SkySkimmer
Reviewed-by: gares
Ack-by: herbelin
Reviewed-by: maximedenes
Reviewed-by: ppedrot
|
|
|
|
|
|
|
|
Reviewed-by: SkySkimmer
|
|
Doesn't seem to matter in practice, but it doesn't hurt either.
|
|
|
|
This prevents having to call global functions, for no good reason.
We also seize the opportunity to name the check argument.
|
|
|
|
Some of them are significant so presumably it will take a bit of
effort to fix overlays.
I left out the removal of `nf_enter` for now as MTac2 needs some
serious porting in order to avoid it.
|
|
The [int] is incorrect for list focusing, we could work a bit harder
to fix that. It's only used for pluralisation in the error message "no
such goal(s)" so we could also ignore the issue.
|
|
We add the information on the proper layer by catching the low-level
exception.
|
|
We perform some cleanup and remove dependency of `proofs/` on
`interp/`, which seems logical.
In fact, `interp` + `parsing` are quite self-contained, so if there is
interest we could also make tactics to depend directly on proofs.
|
|
Ack-by: SkySkimmer
Reviewed-by: ejgallego
Reviewed-by: ppedrot
|
|
|
|
We change the API; after some thinking the tradeoff is clear in favor
of the more radical functional option from the start.
We also guarante the existence of a proof is by typing now,
so exceptions `NoCurrentProof` and `NoSuchGoal` are gone.
TODO: Review what's going on with focusing now.
|
|
|
|
Kernel should be mostly correct, higher levels do random stuff at
times.
|
|
Ack-by: gares
Ack-by: herbelin
Ack-by: mattam82
Ack-by: ppedrot
|
|
I think the usage looks cleaner this way.
|
|
In order to do so we place the polymorphic status and name in the
read-only part of the monad.
Note the added comments, as well as the fact that almost no part of
tactics depends on `proofs` nor `interp`, thus they should be placed
just after pretyping.
Gaëtan Gilbert noted that ideally, abstract should not depend on the
polymorphic status, should we be able to defer closing of the
constant, however this will require significant effort.
Also, we may deprecate nameless abstract, thus rending both of the
changes this PR need unnecessary.
|
|
|
|
|
|
Named evar_abstract_arguments, this field indicates if the evar
arguments corresponding to certain hypothesis can be immitated during
inversion or not. If the argument comes from an abstraction (the evar
was of arrow type), then imitation is disallowed as it gives unnatural
solutions, and lambda abstraction is preferred.
|
|
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.
|
|
|
|
DAG nodes hold now a system state and a parsing state.
The latter is always passed to the parser.
This paves the way to decoupling the effect of commands on the parsing
state and the system state, and hence never force to interpret, say,
Notation.
Handling proof modes is now done explicitly in the STM, not by interpreting
VernacStartLemma.
Similarly Notation execution could be split in two phases in order to obtain a
parsing state without fully executing it (that requires executing all
commands before it).
Co-authored-by: Maxime Dénès <maxime.denes@inria.fr>
Co-authored-by: Emilio Jesus Gallego Arias <e+git@x80.org>
|
|
This error was more or less a debug tool (checking that no tactic breaks
the invariant). But some users may want to support other models, see
https://github.com/Mtac2/Mtac2/pull/139 for an example discussion.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
workers
|
|
- deprecate the old 5-tuple accessor in favor of a view record,
- move `name` and `kind` proof data from `Proof_global` to `Proof`,
this will prove useful in subsequent functionalizations of the
interface, in particular this is what abstract, which lives in the
monads, needs in order no to access global state.
- Note that `Proof.t` and `Proof_global.t` are redundant anyways.
|
