| Commit message (Collapse) | Author | Age |
|---|
| |\ |
|
| |\ \ |
|
| | | |
| | |
| | |
| | |
| | | |
Essentially, we do not reconstruct the named_context_val when the rel_context
is empty.
|
| | | |
| | |
| | |
| | |
| | | |
Before computing the whd_evar-form of the arguments of an evar, we first
check that it is indeed defined.
|
| |\| | |
|
| | | | |
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
composition operator.
Short story:
This pull-request:
(1) removes the definition of the "right-to-left" function composition operator
(2) adds the definition of the "left-to-right" function composition operator
(3) rewrites the code relying on "right-to-left" function composition to rely on "left-to-right" function composition operator instead.
Long story:
In mathematics, function composition is traditionally denoted with ∘ operator.
Ocaml standard library does not provide analogous operator under any name.
Batteries Included provides provides two alternatives:
_ % _
and
_ %> _
The first operator one corresponds to the classical ∘ operator routinely used in mathematics.
I.e.:
(f4 % f3 % f2 % f1) x ≜ (f4 ∘ f3 ∘ f2 ∘ f1) x
We can call it "right-to-left" composition because:
- the function we write as first (f4) will be called as last
- and the function write as last (f1) will be called as first.
The meaning of the second operator is this:
(f1 %> f2 %> f3 %> f4) x ≜ (f4 ∘ f3 ∘ f2 ∘ f1) x
We can call it "left-to-right" composition because:
- the function we write as first (f1) will be called first
- and the function we write as last (f4) will be called last
That is, the functions are written in the same order in which we write and read them.
I think that it makes sense to prefer the "left-to-right" variant because
it enables us to write functions in the same order in which they will be actually called
and it thus better fits our culture
(we read/write from left to right).
|
| | | | |
|
| | | | |
|
| | | | |
|
| | | | |
|
| | | |
| | |
| | |
| | | |
"Context.Named.{to,of}_rel_decl"
|
| | | | |
|
| |\| | |
|
| | | | |
|
| | | |
| | |
| | |
| | | |
"Context.{Rel,Named}.fold_constr"
|
| | | | |
|
| | | | |
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
mainly concerning referring to "Context.{Rel,Named}.get_{id,value,type}" functions.
If multiple modules define a function with a same name, e.g.:
Context.{Rel,Named}.get_type
those calls were prefixed with a corresponding prefix
to make sure that it is obvious which function is being called.
|
| | | | |
|
| | | |
| | |
| | |
| | | |
Suggested by @ppedrot
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | | |
As noted by @ppedrot, the first is redundant. The patch is basically a renaming.
We didn't make the component optional yet, but this could happen in a
future patch.
|
| | |/
|/|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
In some cases prior to this patch, there were two cases for the same
error function, one taking a location, the other not.
We unify them by using an option parameter, in the line with recent
changes in warnings and feedback.
This implies a bit of clean up in some places, but more importantly, is
the preparation for subsequent patches making `Loc.location` opaque,
change that could be use to improve modularity and allow a more
functional implementation strategy --- for example --- of the
beautifier.
|
| |\| |
|
| | |
| |
| |
| |
| |
| |
| |
| | |
Delimit the scope of the failure to ease potential need for debugging
the debugging printer.
Protect against one of the causes of failure (calling
get_family_sort_of with non-synchronized sigma).
|
| | | |
|
| | |\
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
We used to recompute all fresh named contexts for evars before this patch in
the push_rel_context_to_named_context function. This was incurring a linear
penalty and a memory explosion due to the reallocation of many arrays. Now, we
rather remember the context between evar creations by sharing it in the pretyping
environment.
This can be considered as a fix for bug #4964 even though we might do better.
|
| | | | |
|
| | | | |
|
| |/ / |
|
| | |
| |
| |
| | |
This saves a quadratic allocation by replacing arrays with maps.
|
| | |
| |
| |
| |
| | |
In addition to sharing, we also delay the computation of the environment in
a by-need fashion.
|
| | | |
|
| | |
| |
| |
| |
| |
| |
| | |
We remove in particular a dubious use of an environment in fresh name
generation. The code was using the wrong environment in a function only
depending on the rel context which was resetted most of the time. This
might change the generated names in extremely rare occurences.
|
| |/ |
|
| | |
|
| |
|
|
|
|
| |
module)
For the moment, there is an Error module in compilers-lib/ocamlbytecomp.cm(x)a
|
| | |
|
| |
|
|
|
| |
For better error messages. The API change is
backwards compatible, using a new optional argument.
|
| |
|
|
| |
Take advantage that the provided term is always a variable in Equality.is_eq_x.
|
| |
|
|
| |
We do not allocate a closure in the main loop, and do so only when needed.
|
| |
|
|
|
| |
We do not check for presence of a variable in a global definition when we know
that this variable was not present in the section.
|
| |
|
|
|
|
|
|
|
| |
We do not recompute shortest name identifier for global references that were
already traversed. Furthermore, we share the computation of identifiers
between invokations of the name generating function.
This drastically speeds up detyping for huge goals, further mitigating the
shortcomings of the fix for bug #4777.
|
| | |
|
| |
|
|
|
|
|
|
|
|
| |
unshelve_goals is used to correctly register dependent
subgoals that have to be solved. Resolution may fail to
do so using hints, so we have to put them back as goals
in that case. The shelf is a good interface for doing that.
unifiable can be used outside proofview to detect dependencies
between goals. This might be better in another module.
|
| |
|
|
| |
Fix typo in proofview
|
| |\ |
|
| |\ \
| | |
| | |
| | | |
This is the "error resiliency" mode for STM
|
| | | | |
|
| | | | |
|
Pierre-Marie Pédrot
Hugo Herbelin
Matej Kosik
Matej Kosik
Emilio Jesus Gallego Arias
Guillaume Melquiond
Pierre Letouzey
Matthieu Sozeau
Matthieu Sozeau
Enrico Tassi
Cyprien Mangin