| Age | Commit message (Collapse) | Author |
|---|
|
This feature makes it possible to tell type inference to type
applications of a global `foo` using typing information from the context
once the `n` first arguments are known.
The syntax is: `Arguments foo x y | z`.
Closes #7910
|
|
This was introduced by @herbelin in
817308ab59daa40bef09838cfc3d810863de0e46, appears to have been
made unnecessary again by herbelin in
4dab4fc5b2c20e9b7db88aec25a920b56ac83cb6.
At this point it appears to be completely unused.
|
|
We make clearer which arguments are optional and which are mandatory.
Some of these representations are tricky because of small differences
between Program and Function, which share the same infrastructure.
As a side-effect of this cleanup, Program Fixpoint can now be used with
e.g. {measure (m + n) R}. Previously, parentheses were required around
R.
|
|
|
|
|
|
Ack-by: JasonGross
Reviewed-by: ppedrot
|
|
only.
Ack-by: SkySkimmer
Reviewed-by: aspiwack
Ack-by: ejgallego
Ack-by: gares
Ack-by: herbelin
Reviewed-by: mattam82
Ack-by: maximedenes
|
|
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Ack-by: gares
Ack-by: pi8027
|
|
|
|
Previously, they were hard-wired in the ML code.
|
|
The `Coercion` command did report many ambiguous paths when one declared
multiple inheritances. This change makes the `Coercion` command to do not
report them when
1. all the coercion in the potentially ambiguous paths respect the uniform
inheritance condition and
2. functional compositions of the potentially ambiguous paths are convertible to
each other.
The first condition is not explicitly checked but is used to make the checking
process of the second condition easy.
The key idea of this change:
Let us consider a sequence of coercion
f_1 : C_1 >-> C_2, f_2 : C_2 >-> C_3, ..., f_n : C_n >-> C_(n+1)
which respect the uniform inheritance condition and where the user-defined
classes C_i have m_i parameters respectively (i <= n).
The functional composition f_1 . ... . f_n can be expressed as follows:
(fun x_1 ... x_(m_1) y =>
f_n _ ... _ (* m_n times repetition of holes *)
(...
(f_2 _ ... _ (* m_2 times repetition of holes *)
(f_1 x_1 ... x_(m_1) y))...)),
and the contents of all the holes can be determined (inferred) without leaving
any existential variables in them thanks to the uniform inheritance condition.
Misc:
- A test case for this change: test-suite/output/relaxed_ambiguous_paths.v
- Turn the ambiguous paths messages into warnings to do output test.
|
|
Kernel should be mostly correct, higher levels do random stuff at
times.
|
|
Note currently it's impossible to define inductives in SProp because
indtypes.ml and the pretyper aren't fully plugged.
|
|
|
|
Ack-by: gares
Ack-by: herbelin
Ack-by: mattam82
Ack-by: ppedrot
|
|
|
|
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).
|
|
|
|
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.
|
|
Ack-by: JasonGross
Ack-by: SkySkimmer
Ack-by: ejgallego
Ack-by: gares
Ack-by: maximedenes
Ack-by: ppedrot
|
|
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>
|
|
|
|
comments.
|
|
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 :)
|
|
Rename Univ.Level.{Qualid -> UGlobal}, remove Univ.Level.Id.
Remove the ability to split the argument of `Univ.Level.Level` into a
dirpath*int pair (except by going through string hacks like
detyping/pretyping(/funind) does).
Id.of_string_soft to turn unnamed universes into qualid is pushed up
to detyping. (TODO some followup PR clean up more)
This makes it pointless to have an opaque type for ints in
Univ.Level: it would only be used as argument to
Univ.Level.UGlobal.make, ie
~~~
open Univ.Level
let x = UGlobal.make dp (Id.make n)
(* vs *)
let x = UGlobal.make dp n
~~~
Remaining places which create levels from ints are various hacks (eg
the dummy in inductive.ml, the Type.n universes in ugraph
sort_universes) and univgen.
UnivGen does have an opaque type for ints used as univ ids since they
get manipulated by the stm.
NB: build breaks due to ocamldep issue if UGlobal is named Global instead.
|
|
Remote counters were trying to build universe levels (as opposed to
simple integers), but did not have access to the right dirpath at
construction time. We fix it by constructing the level only at use time,
and we introduce some abstractions for qualified and unqualified level
names.
|
|
This makes setting the option outside of the synchronized summary impossible.
|
|
write_function
|
|
|
|
(same for solve_remaining_evars)
This is the standard way to use these functions, with 1 exception in
Unification.
|
|
|
|
functions
|
|
|
|
This emphasizes that it works only on inductive types.
Also, the name is_template_polymorphic will be reused for a more
general version.
|
|
We can then avoid passing an empty env.
|
|
for the determination of evars that can be turned into obligations.
|
|
|
|
|
|
|
|
This builds on the work on #8545. Some tab removal had to take place
here in order to make ocp-indent work.
|
|
This builds on the work on #8545.
|
|
compat updates to do as part of a release.
|
|
Mostly via `dev/tools/update-compat.py --cur-version=8.9`
We just remove test-suite/success/FunindExtraction_compat86.v because,
except for the `Extraction iszero.` line at the bottom, it is a
duplicate of `test-suite/success/Funind.v` (except with `-compat 8.6`).
We also manually update a number of test-suite files to pre-emptively
remove compatibility notations (which used to be compat 8.6, but are now
compat 8.7).
|
|
Fixes #6764: Printing Notation regressed compared to 8.7
|
|
|
|
The functions in `Termops.print_*` are meant to be debug printers,
however, they are sometimes used in non-debug code due to a API
confusion.
We thus wrap such functions into an `Internal` module, improve
documentation, and switch users to the right API.
|
|
variables.
|
|
|
|
When interpreting an existential variable "?n@{inst}" in the current
context, check that variables bound to local definitions are replaced
by variables with convertible body.
Also give a message explaining the type error or non-convertibility
error rather than wrongly saying that there is no binding for the
variable.
|
|
This concerns e.g. "?[id]", "?[?id]" or "?id" (in terms, not in
patterns), so that all names occurring in terms are consistently
interpreted as ltac names.
Moreover, with that, we can for instance do:
Ltac pick x := eexists ?[x].
Goal exists x, x = 0.
pick foo.
|
