| Age | Commit message (Collapse) | Author |
|---|
|
|
|
This is extracted from #9710, where we need the environment anyway to compute
iota rules on inductive types with let-bindings. The commit is self-contained,
so I think it could go directly in to save me a few rebases.
Furthermore, this is also related to #11707. Assuming we split cbn from the
other reduction machine, this allows to merge the "local" machine with
the general one, since after this PR they will have the same type. One less
reduction machine should make people happy.
|
|
Ack-by: SkySkimmer
Reviewed-by: maximedenes
|
|
- Provide new helper functions in `Goptions` on the model of
`declare_bool_option_and_ref`;
- Use these helper functions in many parts of the code base
(encapsulates the corresponding references);
- Move almost all options from `declare_string_option` to
`declare_stringopt_option` (only "Warnings" continue to use the
former). This means that these options now support `Unset` to get
back to the default setting. Note that there is a naming
misalignment since `declare_int_option` is similar to
`declare_stringopt_option` and supports `Unset`. When "Warning" is
eventually migrated to support `Unset` as well, we can remove
`declare_string_option` and rename `declare_stringopt_option` to
`declare_string_option`.
- For some vernac options and flags that have an equivalent
command-line option or flag, implement it like the standard `-set`
and `-unset`.
|
|
This corresponds more naturally to the use we make of them, as we don't need
fast indexation but we instead keep pushing terms on top of them.
|
|
Add headers to a few files which were missing them.
|
|
Reviewed-by: Zimmi48
Reviewed-by: ppedrot
|
|
The standard use is to repeat the option keywords in lowercase, which
is basically useless.
En passant add doc entry for Dump Arith.
|
|
Instead of various termops and globnames aliases.
|
|
Namely, Evd.evar_env and Evd.evar_filtered_env now take an additional
environment instead of querying the imperative global one. We percolate
this change as higher up as possible.
|
|
We also remove trailing whitespace.
Script used:
```bash
for i in `find . -name '*.ml' -or -name '*.mli' -or -name '*.mlg'`; do expand -i "$i" | sponge "$i"; sed -e's/[[:space:]]*$//' -i.bak "$i"; done
```
|
|
Beware of 0. = -0. issue for primitive floats
The IEEE 754 declares that 0. and -0. are treated equal but we cannot
say that this is true with Leibniz equality.
Therefore we must patch the equality and the total comparison inside the
kernel to prevent inconsistency.
|
|
|
|
Fixes #10300 and #10285.
|
|
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.
|
|
|
|
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.
|
|
There is no point, it is always called with refolding turned off.
|
|
In particular evar_eqappr_x tries to find a miller pattern on both sides,
while the fast path for evars tries solve_simple_eqn in one direction
only. So if you have (Evar-not-miller = Evar-miller) the code was not
trying to solve the RHS.
|
|
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.
|
|
|
|
|
|
|
|
|
|
Remaining cases are due to map_constr_with_binders_left_to_right which
does not allow side effects on the evd yet.
|
|
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).
|
|
|
|
|
|
The code is cleaner and more self-explanatory this way.
|
|
It does checking of evar instance and Evd.define, assuming an
occur-check has already been performed.
|
|
|
|
|
|
|
|
|
|
Also extend evarconv to handle frozen evars and flags for delta and
betaiota reduction.
- Make evar_conv unification take a record of flags
- Adds an imitate_defs option to evarsolve, deactivated in first-order unification
- Add a way to call back conv_algo differently on types
- We distinguish comparison of terms and types which might be different
w.r.t. delta reductions allowed (everything for types, controlled for
terms). We keep the with_cs flag even for types, to avoid
incompatibilities (in HoTT's theories/Spaces/No.v, the refine in
No_encode_le_lt would diverge due to trying a default canonical
structure during type verification).
- In evarsolve, do_project_effects checks evar instances now
- Solve evar-evar unification using miller patterns if possible.
- FO heuristic in evarconv
- Do not catch critical exceptions in evarconv
- Force HO matching to abstract toplevel evar args,
This disallows K on them, more compatible with w_unify_to_subterm.
- occur_rigidly improvement, better approx of occur-check.
- K_at_toplevel, subterm_ts, betaiota and frozen_evars flags taken into
account in apply_on_subterm and evar_conv_x.
This allow implementing a unification without reduction, e.g. for the
fast path of rewrite subterm selection.
- second_order_matching works up-to cumulativity
- pretyping/coercion: now take unification flags as argument
- pretyping/unification: default_occurrence_test takes a frozen_evars set
export elim_flags_evars to compute frozen evars before elim
- evarsolve: fix evar_define doing check in the wrong order,
as conv_algo can trigger the definition of the evar itself,
define it first in the evd.
- w_unify: disallow HO in consider_remaining. Only used in rewrite now
- use evar_abstraction info
- catch second_order_matching NoOccurrence exception in second_order_matching_with_args
- unify_with_heuristics in API
- second_order_matching: thin evars after abstraction to put in the
right env or fail.
|
|
|
|
The semantics is obviously that it is an error if not at least one
occurrence is found (natural semantics for rewriting for
example).
|
|
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>
|
|
|
|
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 :)
|
|
|
|
|
|
This is documented in dev/doc/changes.md.
|
|
|
|
|
|
|
|
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>
|
|
A few of them will be of help for future cleanups. We have spared the
stuff in `Names` due to bad organization of this module following the
split from `Term`, which really difficult things removing the
constructors.
|
