| Age | Commit message (Collapse) | Author |
|---|
|
|
|
We remove `edit_id` from the STM. In PIDE they serve a different
purpose, however in Coq they were of limited utility and required many
special cases all around the code.
Indeed, parsing is not an asynchronous operation in Coq, thus having
feedback about parsing didn't make much sense. All clients indeed
ignore such feedback and handle parsing in a synchronous way.
XML protocol clients are unaffected, they rely on the instead on the
Fail value.
This commit supersedes PR#203.
|
|
|
|
|
|
|
|
Instead of browsing the term as many times as there are abstracted constants,
we replace the constants in one pass. We have to be a bit careful to replace
the right variables though, in case there are chained abstracts. This is much
faster.
This solves the second part of bug #5382: Huge case analysis fails in coq8.5.x.
|
|
We don't need to look for the size of the whole list to find whether we can
extract a suffix from it, as we can do it in one go instead. This slowness
was observable in abstract-heavy code.
|
|
In one case, the hashconsed type of a judgement was not used anywhere else.
In another case, the Opaqueproof module was rehashconsing terms that had
already gone through a hashconsing phase. Indeed, most OpaqueDef constructor
applications actually called it beforehand, so that the one performed in
Opaqueproof was most often useless. The only case where this was not true
was at section closing time, so that we tweak the Cooking.cook_constant to
perform hashconsing for us.
|
|
|
|
We were doing fishy things in the Term_typing file, where side-effects were
not considered in the right uniquization order because of the uniq_seff_rev
function. It probably did not matter after a9b76df because effects were
(mostly) uniquize upfront, but this is not clear because of the use of the
transparente API in the module.
Now everything has to go through the opaque API, so that a proper dependence
order is ensured.
|
|
We move it from Entries to Term_typing and export the few functions needed
to manipulate it in this module.
|
|
|
|
|
|
I believe an unwanted shadowing was introduced by a4043608f704f0.
|
|
|
|
No functional change, we create the new string beforehand and
`id_of_string` will become a noop with `-safe-string`.
|
|
It was always set to `greedy:true`.
|
|
This is really [mv fast_typeops.ml{,i} typeops.ml{,i}] plus trivial
changes in the other files, the real changes are in the parent commit.
|
|
|
|
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.{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.
|
|
module)
For the moment, there is an Error module in compilers-lib/ocamlbytecomp.cm(x)a
|
|
|
|
|
|
This allows a smooth addition of various unsafe flags without wreaking
havoc in the ML codebase.
|
|
|
|
The rational is that
1. further typing flags may be available in the future
2. it makes it easier to trace and document the argument
|
|
This patch splits pretty printing representation from IO operations.
- `Pp` is kept in charge of the abstract pretty printing representation.
- The `Feedback` module provides interface for doing printing IO.
The patch continues work initiated for 8.5 and has the following effects:
- The following functions in `Pp`: `pp`, `ppnl`, `pperr`, `pperrnl`,
`pperr_flush`, `pp_flush`, `flush_all`, `msg`, `msgnl`, `msgerr`,
`msgerrnl`, `message` are removed. `Feedback.msg_*` functions must be
used instead.
- Feedback provides different backends to handle output, currently,
`stdout`, `emacs` and CoqIDE backends are provided.
- Clients cannot specify flush policy anymore, thus `pp_flush` et al are
gone.
- `Feedback.feedback` takes an `edit_or_state_id` instead of the old
mix.
Lightly tested: Test-suite passes, Proof General and CoqIDE seem to work.
|
|
|
|
Fixes compilation of Coq with OCaml 4.03 beta 1.
|
|
Originally, rel-context was represented as:
Context.rel_context = Names.Name.t * Constr.t option * Constr.t
Now it is represented as:
Context.Rel.t = LocalAssum of Names.Name.t * Constr.t
| LocalDef of Names.Name.t * Constr.t * Constr.t
Originally, named-context was represented as:
Context.named_context = Names.Id.t * Constr.t option * Constr.t
Now it is represented as:
Context.Named.t = LocalAssum of Names.Id.t * Constr.t
| LocalDef of Names.Id.t * Constr.t * Constr.t
Motivation:
(1) In "tactics/hipattern.ml4" file we define "test_strict_disjunction"
function which looked like this:
let test_strict_disjunction n lc =
Array.for_all_i (fun i c ->
match (prod_assum (snd (decompose_prod_n_assum n c))) with
| [_,None,c] -> isRel c && Int.equal (destRel c) (n - i)
| _ -> false) 0 lc
Suppose that you do not know about rel-context and named-context.
(that is the case of people who just started to read the source code)
Merlin would tell you that the type of the value you are destructing
by "match" is:
'a * 'b option * Constr.t (* worst-case scenario *)
or
Named.Name.t * Constr.t option * Constr.t (* best-case scenario (?) *)
To me, this is akin to wearing an opaque veil.
It is hard to figure out the meaning of the values you are looking at.
In particular, it is hard to discover the connection between the value
we are destructing above and the datatypes and functions defined
in the "kernel/context.ml" file.
In this case, the connection is there, but it is not visible
(between the function above and the "Context" module).
------------------------------------------------------------------------
Now consider, what happens when the reader see the same function
presented in the following form:
let test_strict_disjunction n lc =
Array.for_all_i (fun i c ->
match (prod_assum (snd (decompose_prod_n_assum n c))) with
| [LocalAssum (_,c)] -> isRel c && Int.equal (destRel c) (n - i)
| _ -> false) 0 lc
If the reader haven't seen "LocalAssum" before, (s)he can use Merlin
to jump to the corresponding definition and learn more.
In this case, the connection is there, and it is directly visible
(between the function above and the "Context" module).
(2) Also, if we already have the concepts such as:
- local declaration
- local assumption
- local definition
and we describe these notions meticulously in the Reference Manual,
then it is a real pity not to reinforce the connection
of the actual code with the abstract description we published.
|
|
|
|
|
|
|
|
The structure of the Context module was refined in such a way that:
- Types and functions related to rel-context declarations were put into the Context.Rel.Declaration module.
- Types and functions related to rel-context were put into the Context.Rel module.
- Types and functions related to named-context declarations were put into the Context.Named.Declaration module.
- Types and functions related to named-context were put into the Context.Named module.
- Types and functions related to named-list-context declarations were put into Context.NamedList.Declaration module.
- Types and functions related to named-list-context were put into Context.NamedList module.
Some missing comments were added to the *.mli file.
The output of ocamldoc was checked whether it looks in a reasonable way.
"TODO: cleanup" was removed
The order in which are exported functions listed in the *.mli file was changed.
(as in a mature modules, this order usually is not random)
The order of exported functions in Context.{Rel,Named} modules is now consistent.
(as there is no special reason why that order should be different)
The order in which are functions defined in the *.ml file is the same as the order in which they are listed in the *.mli file.
(as there is no special reason to define them in a different order)
The name of the original fold_{rel,named}_context{,_reverse} functions was changed to better indicate what those functions do.
(Now they are called Context.{Rel,Named}.fold_{inside,outside})
The original comments originally attached to the fold_{rel,named}_context{,_reverse} did not full make sense so they were updated.
Thrown exceptions are now documented.
Naming of formal parameters was made more consistent across different functions.
Comments of similar functions in different modules are now consistent.
Comments from *.mli files were copied to *.ml file.
(We need that information in *.mli files because that is were ocamldoc needs it.
It is nice to have it also in *.ml files because when we are using Merlin and jump to the definion of the function,
we can see the comments also there and do not need to open a different file if we want to see it.)
When we invoke ocamldoc, we instruct it to generate UTF-8 HTML instead of (default) ISO-8859-1.
(UTF-8 characters are used in our ocamldoc markup)
"open Context" was removed from all *.mli and *.ml files.
(Originally, it was OK to do that. Now it is not.)
An entry to dev/doc/changes.txt file was added that describes how the names of types and functions have changed.
|
|
|
|
The side-effects can contain universe declarations needed to typecheck
later proofs, which weren't added to the env used to typecheck them.
|
|
|
|
Side effects are now an opaque data type, called private_constant, you can
only obtain from safe_typing. When add_constant is called on a
definition_entry that contains private constants, they are either
- inlined in the main proof term but not re-checked
- declared globally without re-checking them
As a safety measure, the opaque data type contains a pointer to the
revstruct (an internal field of safe_env that changes every time a new
constant is added), and such pointer is compared with the current value
store in safe_env when the private_constant is inlined. Only when the
comparison is successful the private_constant is not re-checked. Otherwise
else it is. In short, we accept into the kernel private constant only
when they arrive in the very same order and on top of the very same env
they arrived when we fist checked them.
Note: private_constants produced by workers never pass the safety
measure (the revstruct pointer is an Ephemeron). Sending back the
entire revstruct is possible but: 1. we lack a way to quickly compare
two revstructs, 2. it can be large.
|
|
polymorphic definitions.
- This implementation passes universes in separate arguments and does not
eagerly instanitate polymorphic definitions.
- This means that it pays no cost on monomorphic definitions.
|
|
- "Proof using p*" means: use p and any section var about p.
- Simplify the grammar/parser for proof using <expression>.
- Section variables with a body (let-in) are pulled in automatically
since they are safe to be used (add no extra quantification)
- automatic clear of "unused" section variables made optional:
Set Proof Using Clear Unused.
since clearing section hypotheses does not "always work" (e.g. hint
databases are not really cleaned)
- term_typing: trigger a "suggest proof using" message also for Let
theorems.
|
|
Given the way Lib.extract_hyps is coded if the const_hyps field
of a constant declaration contains a named_context that does not
have the same order of the one in Environment.env, discharging is
broken (as in some section variables are not discharged).
If const_hyps is computed by the kernel, then the order is correct by
construction. If such list is provided by the user, the order is not
granted.
We now systematically sort the list of user provided section hyps.
The code of Proof using is building the named_context in the right
order, but the API was not enforcing/checking it. Now it does.
|
|
|
|
|
|
assumed.
|
|
The path is quite a bit of a maze, this commit is not as simple as it ought to be. Something more robust than a boolean should be used here.
|
|
I'm pushing this patch now because the previous treatment of such projections
in the VM was already unsound. It should however be carefully reviewed.
|
