aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel
Commit message (Collapse)AuthorAge
* [VM] Remove projection names from structured constants.Gravatar Maxime Dénès2018-06-10
| | | | | | | It was actually a hack since those names are never used to represent values, only to be passed as arguments to bytecode instructions. So instead of reusing the structured_constant type, we follow the same pattern as switch annotations.
* More straightforward native compilation of primitive projections.Gravatar Pierre-Marie Pédrot2018-06-05
| | | | | | Instead of having a constant-based compilation of projections, we generate them at the compilation time of the inductive block to which they pertain.
* Use projection indices in native compilation rather than constant names.Gravatar Pierre-Marie Pédrot2018-06-05
|
* Merge PR #7643: Fix #7631: native_compute fails to compile an example in Coq 8.8Gravatar Pierre-Marie Pédrot2018-06-05
|\
* \ Merge PR #7646: Fix #4714: Stack overflow with native computeGravatar Pierre-Marie Pédrot2018-06-05
|\ \
* \ \ Merge PR #7495: Fix restrict_universe_contextGravatar Matthieu Sozeau2018-06-05
|\ \ \
| | | * Fix #7631: native_compute fails to compile an example in Coq 8.8Gravatar Maxime Dénès2018-06-04
| |_|/ |/| | | | | | | | | | | Dependency analysis for separate compilation was not iterated properly on rel_context and named_context.
* | | Merge PR #7418: Actually take advantage of the normalization status of ↵Gravatar Maxime Dénès2018-06-04
|\ \ \ | | | | | | | | | | | | kernel closures.
* \ \ \ Merge PR #7496: Fix #4403: insufficient handling of type-in-type in kernel.Gravatar Maxime Dénès2018-06-04
|\ \ \ \
* \ \ \ \ Merge PR #7234: Reduce circular dependency constants <-> projectionsGravatar Maxime Dénès2018-06-01
|\ \ \ \ \
| | | | | * Fix #4714: Stack overflow with native computeGravatar Maxime Dénès2018-05-31
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Values containing (retroknowledge-based) matchine integers were not recognized as literals.
| * | | | | Reduce circular dependency constants <-> projectionsGravatar Gaëtan Gilbert2018-05-31
| | |_|_|/ | |/| | | | | | | | | | | | | | | | | | Instead of having the projection data in the constant data we have it independently in the environment.
* | | | | [api] Remove deprecated object from `Term`Gravatar Emilio Jesus Gallego Arias2018-05-30
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We remove most of what was deprecated in `Term`. Now, `intf` and `kernel` are almost deprecation-free, tho I am not very convinced about the whole `Term -> Constr` renaming but I'm afraid there is no way back. Inconsistencies with the constructor policy (see #6440) remain along the code-base and I'm afraid I don't see a plan to reconcile them. The `Sorts` deprecation is hard to finalize, opening `Sorts` is not a good idea as someone added a `List` module inside it.
* | | | | [api] Remove deprecated aliases from `Names`.Gravatar Emilio Jesus Gallego Arias2018-05-30
| | | | |
* | | | | [api] Reintroduce `Names.global_reference` aliasGravatar Emilio Jesus Gallego Arias2018-05-30
|/ / / / | | | | | | | | | | | | | | | | | | | | | | | | Due to a bad interaction between PRs, the `Names.global_reference` alias was removed in 8.9, where it should disappear in 8.10. The original PR #6156 deprecated the alias in `Libnames`.
| | | * Fix restrict_universe_contextGravatar Gaëtan Gilbert2018-05-30
| |_|/ |/| |
* | | Fix #7333: vm_compute segfaults / Anomaly with cofixGravatar Maxime Dénès2018-05-28
| | | | | | | | | | | | | | | We eta-expand cofixpoints when needed, so that their call-by-need evaluation is correctly implemented by VM and native_compute.
* | | Unify pre_env and envGravatar Maxime Dénès2018-05-28
| | | | | | | | | | | | | | | We now have only two notions of environments in the kernel: env and safe_env.
* | | Remove vm_conv hook and reorganize kernel filesGravatar Maxime Dénès2018-05-28
| | |
* | | Make some comments more precise about compilation of cofixpointsGravatar Maxime Dénès2018-05-28
| | |
* | | Less confusing debug printing of setfield bytecode instructionGravatar Maxime Dénès2018-05-28
| | |
* | | Merge pull request #7569 from ppedrot/clean-newringGravatar Assia Mahboubi2018-05-25
|\ \ \ | | | | | | | | Simplify the newring hack
* | | | Renaming miscellaneous internal smart functions.Gravatar Hugo Herbelin2018-05-23
| | | |
* | | | Moving Rtree.smart_map into Rtree.Smart.map.Gravatar Hugo Herbelin2018-05-23
| | | |
* | | | Moving Option.smart_map to Option.Smart.map.Gravatar Hugo Herbelin2018-05-23
| | | |
* | | | Collecting List.smart_* functions into a module List.Smart.Gravatar Hugo Herbelin2018-05-23
| | | |
* | | | Exporting Fun1 within Array so that Array.Fun1 and not only CArray.Fun1 works.Gravatar Hugo Herbelin2018-05-23
| | | |
* | | | Collecting Array.smart_* functions into a module Array.Smart.Gravatar Hugo Herbelin2018-05-23
| | | |
| * | | Simplify the newring hack.Gravatar Pierre-Marie Pédrot2018-05-21
|/ / / | | | | | | | | | | | | | | | The new implementation is 100% compatible with the previous one, but it is more compact and does not use a tricky translation function from the kernel.
* | | Merge PR #7079: Remove naked pointers from the VMGravatar Maxime Dénès2018-05-16
|\ \ \
| | * | Fix #4403: insufficient handling of type-in-type in kernel.Gravatar Gaëtan Gilbert2018-05-13
| |/ / |/| |
* | | [api] Rename `global_reference` to `GlobRef.t` to follow kernel style.Gravatar Emilio Jesus Gallego Arias2018-05-04
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | In #6092, `global_reference` was moved to `kernel`. It makes sense to go further and use the current kernel style for names. This has a good effect on the dependency graph, as some core modules don't depend on library anymore. A question about providing equality for the GloRef module remains, as there are two different notions of equality for constants. In that sense, `KerPair` seems suspicious and at some point it should be looked at.
| | * Actually take advantage of the normalization status of kernel closures.Gravatar Pierre-Marie Pédrot2018-05-01
| |/ |/| | | | | | | | | | | | | | | | | | | | | We know that when a fterm is marked as Whnf or Norm, the only thing that can happen in the reduction machine is administrative reduction pushing the destructured term on the stack. Thus there is no need to perform any actual performative reduction. Furthermore, every head subterm of those terms are recursively Whnf or Norm, which implies that no update mark is pushed on the stack during the destructuration. So there is no need to unzip the stack to unset FLOCKED nodes as well.
| * Adapt the VM GC hook to handle the no-naked-pointers option flag.Gravatar Pierre-Marie Pédrot2018-04-30
| | | | | | | | | | | | | | The Coq VM stack is scanned by the OCaml GC, but it can contain raw pointers to C-allocated strings standing for VM bytecode. If the the no-naked-pointers option is set, we perform the check that a stack value lives on the OCaml heap ourselves.
| * Make the VM accumulator look like an OCaml block.Gravatar Pierre-Marie Pédrot2018-04-30
| | | | | | | | | | | | We allocate an additional header so that the accumulator is not a naked pointer. Indeed, it is contained in accumulator blocks which are scanned by the GC as their tags is 0.
| * Wrap VM bytecode used on the OCaml side in an OCaml block.Gravatar Pierre-Marie Pédrot2018-04-30
|/ | | | | | | | | | This prevents the existence of a few naked pointers to C heap from the OCaml heap. VM bytecode is represented as any block of size at least 1 whose first field points to a C-allocated string. This representation is compatible with the Coq VM representation of (potentially recursive) closures, which are already specifically tailored in the OCaml GC to be able to contain out-of-heap data.
* Merge PR #6958: [lib] Move global options to their proper place.Gravatar Maxime Dénès2018-04-30
|\
* \ Merge PR #6892: Cleanup implementation of normalize_context_set a bitGravatar Pierre-Marie Pédrot2018-04-28
|\ \
* | | Always print explanation for univ inconsistency, rm Flags.univ_printGravatar Gaëtan Gilbert2018-04-26
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This removes the Flags.univ_print in the kernel, making it possible to put the univ printing flag ownership back in Detyping. The lazyness is because getting an explanation may be costly and we may discard it without printing. See benches - with lazy https://ci.inria.fr/coq/view/benchmarking/job/benchmark-part-of-the-branch/406/console - without lazy https://ci.inria.fr/coq/view/benchmarking/job/benchmark-part-of-the-branch/405/console Notably without lazy mathcomp odd_order is +1.26% with some lines showing significant changes, eg PFsection11 line 874 goes from 11.76s to 13.23s (+12%). (with lazy the same development has -1% overall and the same line goes from 11.76s to 11.23s (-4%) which may be within noise range)
* | | Merge PR #6908: Move VM global tables from C to MLGravatar Maxime Dénès2018-04-20
|\ \ \
| | * | universe normalisation: put equivalence class partition in UGraphGravatar Gaëtan Gilbert2018-04-13
| |/ / |/| | | | | | | | ie don't go through having Eq constraints but directly to the unionfind.
* | | Merge PR #6972: [api] Deprecate a couple of aliases that we missed.Gravatar Maxime Dénès2018-04-12
|\ \ \
* \ \ \ Merge PR #7176: Fix #6956: Uncaught exception in bytecode compilationGravatar Pierre-Marie Pédrot2018-04-09
|\ \ \ \
| * | | | Fix #6956: Uncaught exception in bytecode compilationGravatar Maxime Dénès2018-04-06
| | | | | | | | | | | | | | | | | | | | We also make the code of [compact] in kernel/univ.ml a bit clearer.
| | | | * [lib] Move global options to their proper place.Gravatar Emilio Jesus Gallego Arias2018-04-02
| | |_|/ | |/| | | | | | | | | | | | | | | | | | | | | | | | | | Recent commits introduced global flags, but these should be module-specific so relocating. Global flags are deprecated, and for 8.9 `Lib.Flags` will be reduced to the truly global stuff.
| | * | [api] Deprecate a couple of aliases that we missed.Gravatar Emilio Jesus Gallego Arias2018-03-28
| |/ /
* / / Expliciting and taking advantage of a representation invariant in Esubst.Gravatar Pierre-Marie Pédrot2018-03-27
|/ /
| * More efficient reallocation of VM global tables.Gravatar Pierre-Marie Pédrot2018-03-26
| | | | | | | | | | | | The previous code was mimicking what the C implementation was doing, which was a quadratic algorithm. We simply use the good old exponential reallocation strategy that is amortized O(1).
| * Moving the VM global atom table to a ML reference.Gravatar Pierre-Marie Pédrot2018-03-26
| |
| * Moving the VM global data to a ML reference.Gravatar Pierre-Marie Pédrot2018-03-26
|/
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-29 01:02:17 +0000