| Age | Commit message (Collapse) | Author |
|---|
|
Strangely enough, the checker seems to rely on an outdated decompose_app
function which is not the same as the kernel, as the latter is sensitive
to casts. Cast-manipulating functions from the kernel are only used on
upper layers, and thus was moved there.
|
|
We return an option type, as constraints were always dropped if the boolean
was false. They did not make much sense anyway.
|
|
|
|
Before this patch, this module was a member of the library folder, which had
little to do with its actual use. A tiny part relative to global registering
of universe names has been effectively moved to the Global module.
|
|
|
|
|
|
Was PR#321: Handling of section variables in hints
|
|
|
|
|
|
|
|
|
|
|
|
|
|
due to cleared/reverted section variables.
This fixes the get_type_of but requires keeping information
around about the section hyps available in goals during resolution.
It's optimized for the non-section case (should incur no cost there),
and the case where no section variables are cleared.
|
|
This function does the same thing as "Names.Id.List.mem" so:
- I deleted the "Namegen.to_avoid" function and
- replaced all calls of "Namegen.to_avoid" to calls of "Names.Id.List.mem"
|
|
The word "increment" is more appropriate in this case than "lifting".
The world "lifting", in computer science, usually denotes something else:
https://en.wikipedia.org/wiki/Lambda_lifting
|
|
|
|
When printing evar constraints, we ensure that every variable from the
rel context has a name.
|
|
|
|
|
|
|
|
|
|
Was PR#263: Fast lookup in named contexts
|
|
|
|
goal is under focus and which support returning a relevant output.
|
|
|
|
|
|
|
|
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.
|
|
|
