| Age | Commit message (Collapse) | Author |
|---|
|
![proof_stack] is equivalent to the old meaning of ![proof]: the body
has type `pstate:Proof_global.t option -> Proof_global.t option`
The other specifiers are for the following body types:
~~~
![open_proof] `is_ontop:bool -> pstate`
![maybe_open_proof] `is_ontop:bool -> pstate option`
![proof] `pstate:pstate -> pstate`
![proof_opt_query] `pstate:pstate option -> unit`
![proof_query] `pstate:pstate -> unit`
~~~
The `is_ontop` is only used for the warning message when declaring a
section variable inside a proof, we could also just stop warning.
The specifiers look closely related to stm classifiers, but currently
they're unconnected. Notably this means that a ![proof_query] doesn't
have to be classified QUERY.
![proof_stack] is only used by g_rewrite/rewrite whose behaviour I
don't fully understand, maybe we can drop it in the future.
For compat we may want to consider keeping ![proof] with its old
meaning and using some new name for the new meaning. OTOH fixing
plugins to be stricter is easier if we change it as the errors tell us
where it's used.
|
|
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 never use this id in rewrite.ml so don't bother threading it around.
|
|
|
|
|
|
It's used a few times in the stdlib (a couple of which need no other
change when removing the !) and not at all throughout our CI.
Considering that I think it's fair enough to remove it.
|
|
|
|
|
|
The current situation is a mess, some functions set it by default, but other
no. Making it mandatory ensures that the expected value is the correct one.
|
|
|
|
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.
|
|
|
|
We add state handling to tactics.
TODO:
- [rewrite] `add_morphism_infer` creates problems as it opens a proof.
- [g_obligations] with_tac
|
|
Kernel should be mostly correct, higher levels do random stuff at
times.
|
|
Ack-by: gares
Ack-by: herbelin
Ack-by: mattam82
Ack-by: ppedrot
|
|
Supersedes #8718.
|
|
I think the usage looks cleaner this way.
|
|
Now the main functions are unify (solves the problems entirely) and
unify_delay and unify_leq (which might leave some unsolved constraints).
Deprecated the_conv_x and the_conv_x_leq (which were misnommers as they
do unification not conversion).
|
|
|
|
- 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.
|
|
This is a pre-requisite to use automated formatting tools such as
`ocamlformat`, also, there were quite a few places where the comments
had basically no effect, thus it was confusing for the developer.
p.s: Reading some comments was a lot of fun :)
|
|
We make `declaration_hook`s optional arguments everywhere, and thus we
avoid some "fake" functions having to be passed.
This identifies positively the code really using hooks [funind,
rewrite, coercions, program, and canonicals] and helps moving toward
some hope of reification.
|
|
|
|
|
|
This is documented in dev/doc/changes.md.
|
|
|
|
This provides several advantages to people serializing tactic
scripts. Appearance of the involved constructors is common enough as
to bother to submit this PR.
|
|
|
|
|
|
This is a step towards limiting calls to the global environment.
Incidentally unify naming evd -> sigma in Termops.
|
|
This avoids all the side effects associated with the manipulation of an
unresolvable flag. In the new design:
- The evar_map stores a set of evars that are candidates for typeclass
resolution, which can be retrieved and set.
We maintain the invariant that it always contains only undefined
evars.
- At the creation time of an evar (new_evar), we classify it as a
potential candidate of resolution.
- This uses a hook to test if the conclusion ends in a typeclass
application. (hook set in typeclasses.ml)
- This is an approximation if the conclusion is an existential (i.e.
not yet determined). In that case we register the evar as
potentially a typeclass instance, and later phases must consider
that case, dropping the evar if it is not a typeclass.
- One can pass the ~typeclass_candidate:false flag to new_evar to
prevent classification entirely. Typically this is for new goals
which should not ever be considered to be typeclass resolution
candidates.
- One can mark a subset of evars unresolvable later if
needed. Typically for clausenv, and marking future goals as
unresolvable even if they are typeclass goals. For clausenv for
example, after turing metas into evars we first (optionally) try a
typeclass resolution on the newly created evars and only then mark
the remaining newly created evars as subgoals. The intent of the
code looks clearer now.
This should prevent keeping testing if undefined evars are classes
all the time and crawling large sets when no typeclasses are present.
- Typeclass candidate evars stay candidates through
restriction/evar-evar solutions.
- Evd.add uses ~typeclass_candidate:false to avoid recomputing if the new
evar is a candidate. There's a deficiency in the API, in most use
cases of Evd.add we should rather use a:
`Evd.update_evar_info : evar_map -> Evar.t -> (evar_info -> evar_info)
-> evar_map`
Usually it is only about nf_evar'ing the evar_info's contents, which
doesn't change the evar candidate status.
- Typeclass resolution can now handle the set of candidates
functionally: it always starts from the set of candidates (and not the
whole undefined_map) and a filter on it, potentially splitting it in
connected components, does proof search for each component in an
evar_map with an empty set of typeclass evars (allowing clean
reentrancy), then reinstates the potential remaining unsolved
components and filtered out typeclass evars at the end of
resolution.
This means no more marking of resolvability/unresolvability
everywhere, and hopefully a more efficient implementation in general.
- This is on top of the cleanup of evar_info's currently but can
be made independent.
[typeclasses] Fix cases.ml: none of the new_evars should be typeclass candidates
Solve bug in inheritance of flags in evar-evar solutions.
Renaming unresolvable to typeclass_candidate (positive) and fix maybe_typeclass_hook
|
|
|
|
We refactor the `Coqlib` API to locate objects over a namespace
`module.object.property`.
This introduces the vernacular command `Register g as n` to expose the
Coq constant `g` under the name `n` (through the `register_ref`
function). The constant can then be dynamically located using the
`lib_ref` function.
Co-authored-by: Emilio Jesús Gallego Arias <e+git@x80.org>
Co-authored-by: Maxime Dénès <mail@maximedenes.fr>
Co-authored-by: Vincent Laporte <Vincent.Laporte@fondation-inria.fr>
|
|
It was only used in ltac/rewrite which as a plugin is too late to
affect init.
|
|
|
|
reference was defined as Ident or Qualid, but the qualid type already
permits empty paths. So we had effectively two representations for
unqualified names, that were not seen as equal by eq_reference.
We remove the reference type and replace its uses by qualid.
|
|
- move_location to proofs/logic.
- intro_pattern_naming to Namegen.
|
|
We address the easy ones, but they should probably be all removed.
|
|
|
|
We bootstrap the circular evar_map <-> econstr dependency by moving
the internal EConstr.API module to Evd.MiniEConstr. Then we make the
Evd functions use econstr.
|
|
The `reference` type contains some ad-hoc locations in its
constructors, but there is no reason not to handle them with the
standard attribute container provided by `CAst.t`.
An orthogonal topic to this commit is whether the `reference` type
should contain a location or not at all.
It seems that many places would become a bit clearer by splitting
`reference` into non-located `reference` and `lreference`, however
some other places become messier so we maintain the current status-quo
for now.
|
|
UState normalize -> minimize, Evd nf_constraints -> minimize_universes
|
|
|
|
|
|
|
|
This commit was motivated by true spurious conversions arising in my
`to_constr` debug branch.
The changes here need careful review as the tradeoffs are subtle and
still a lot of clean up remains to be done in `vernac/*`.
We have opted for penalize [minimally] the few users coming from true
`Constr`-land, but I am sure we can tweak code in a much better way.
In particular, it is not clear if internalization should take an
`evar_map` even in the cases where it is not triggered, see the
changes under `plugins` for a good example.
Also, the new return type of `Pretyping.understand` should undergo
careful review.
We don't touch `Impargs` as it is not clear how to proceed, however,
the current type of `compute_implicits_gen` looks very suspicious as
it is called often with free evars.
Some TODOs are:
- impargs was calling whd_all, the Econstr equivalent can be either
+ Reductionops.whd_all [which does refolding and no sharing]
+ Reductionops.clos_whd_flags with all as a flag.
|
|
|
|
We follow the suggestions in #402 and turn uses of `Loc.located` in
`vernac` into `CAst.t`. The impact should be low as this change mostly
affects top-level vernaculars.
With this change, we are even closer to automatically map a text
document to its AST in a programmatic way.
|
|
|
