| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
| |
This is much more efficient than using Nativevalues.is_accu function which
incurs a lot of irrelevant checks on its argument.
|
| | |
|
| |
|
|
|
| |
No need to roll up a new data structure when Environment has O(log n) add
and lookup of rel definitions.
|
| | |
|
| | |
|
| |
|
|
| |
It's a bit shorter and more direct.
|
| |
|
|
|
|
| |
Not sure it could have led to a soundness bug, but this is definitely
serious enough to deserve a backport. Also made the code robust by
listing all the constructors.
|
| |
|
|
|
| |
This brings more compatibility with handling of mutual primitive records
in the kernel.
|
| |
|
|
|
| |
This is a first step towards the acceptance of mutual record types in the
kernel.
|
| |
|
|
|
|
| |
Instead of having a constant-based compilation of projections, we
generate them at the compilation time of the inductive block to which
they pertain.
|
| | |
|
| |
|
|
|
| |
Dependency analysis for separate compilation was not iterated properly
on rel_context and named_context.
|
| |
|
|
|
| |
Instead of having the projection data in the constant data we have it
independently in the environment.
|
| |
|
|
|
| |
We now have only two notions of environments in the kernel: env and
safe_env.
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
| |
We take advantage of the range structure to get a O(log n) retrieval of values
bound to a rel in an environment.
|
| |
|
|
| |
We do up to `Term` which is the main bulk of the changes.
|
| |
|
|
| |
This will allow to merge back `Names` with `API.Names`
|
| |
|
|
| |
This is a first step towards some of the solutions proposed in #6008.
|
| |
|
|
|
| |
Indeed OCaml has a similar file and this conflicts, at least in
debugger.
|
| |
|
|
|
|
| |
Instead of returning either an instance or the set of constraints, we rather
return the corresponding abstracted context. We also push back all uses of
abstraction-breaking calls from these functions out of the kernel.
|
| |
|
|
|
|
| |
This function breaks the abstraction barrier of abstract universe contexts,
as it provides a way to observe the bound names of such a context. We remove
all the uses that can be easily get rid of with the current API.
|
| |
|
|
|
|
| |
Global declarations used to carry universe instances with them, but it
turns out this information is not used anywhere. Instead, instances were
already properly encoded as the first argument of polymorphic definitions.
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
As per https://github.com/coq/coq/pull/716#issuecomment-305140839
Partially using
```bash
git grep --name-only 'anomaly\s*\(~label:"[^"]*"\s*\)\?\(Pp.\)\?(\(\(Pp.\)\?str\)\?\s*".*[^\.!]")' | xargs sed s'/\(anomaly\s*\(~label:"[^"]*"\s*\)\?\(Pp.\)\?(\(\(Pp.\)\?str\)\?\s*".*\s*[^\.! ]\)\s*")/\1.")/g' -i
```
and
```bash
git grep --name-only ' !"' | xargs sed s'/ !"/!"/g' -i
```
The rest were manually edited by looking at the results of
```bash
git grep anomaly | grep '\.ml' | grep -v 'anomaly\s*\(~label:"[^"]*"\s*\)\?\(Pp\.\)\?(\(\(Pp.\)\?str\)\?\s*".*\(\.\|!\)")' | grep 'anomaly\($\|[^_]\)' | less
```
|
| | |
|
| | |
|
| |\ |
|
| | |
| |
| |
| |
| |
| | |
Was introduced by 4f041384cb27f0d2. Unsoundness seems miraculously
avoided by a safeguard I put in nativecode.ml. But other kernel changes
in this commit should probably be reviewed carefully.
|
| |\| |
|
| | |\
| | |
| | |
| | | |
Was PR#263: Fast lookup in named contexts
|
| |\| | |
|
| | |\ \ |
|
| | | | | |
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
The greatest danger of OCaml's polymorphic equality is that PMP can
replace it with pointer equality at any time, be warned :)
The lack of optimization may account for an exponential blow-up in size
of the generated code, as well as worse runtime performance.
|
| | | |/
| |/| |
|
| |\| | |
|
| | | |
| | |
| | |
| | | |
Spotted by PMP.
|
| |/ /
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
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.
|
| | |
| |
| |
| |
| |
| | |
module)
For the moment, there is an Error module in compilers-lib/ocamlbytecomp.cm(x)a
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
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.
|
| | | |
|
| | | |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
...
...
...
...
...
...
...
...
...
...
...
...
...
...
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
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.
|
| |\| |
|
| | | |
|
Pierre-Marie Pédrot
Gaëtan Gilbert
Gaëtan Gilbert
Maxime Dénès
Théo Zimmermann
Emilio Jesus Gallego Arias
Hugo Herbelin
Amin Timany
Jason Gross
Matej Kosik
Pierre Letouzey
Matej Kosik