aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel
Commit message (Collapse)AuthorAge
* [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 #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
|\
* | [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.
| * 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
|/
* Fix expected number of arguments for cumulative constructors.Gravatar Gaëtan Gilbert2018-03-09
| | | | | | | We expected `nparams + nrealargs + consnrealargs` but the `nrealargs` should not be there. This breaks cumulativity of constructors for any inductive with indices (so records still work, explaining why the test case in #6747 works).
* Merge PR #6775: Allow using cumulativity without forcing strict constraints.Gravatar Maxime Dénès2018-03-09
|\
* \ Merge PR #6769: Split closure cache and remove whd_bothGravatar Maxime Dénès2018-03-09
|\ \
| | * Cumulativity: improve treatment of irrelevant universes.Gravatar Gaëtan Gilbert2018-03-09
| | | | | | | | | | | | | | | | | | In Reductionops.infer_conv we did not have enough information to properly try to unify irrelevant universes. This requires changing the Reduction.universe_compare type a bit.
| | * Allow using cumulativity without forcing strict constraints.Gravatar Gaëtan Gilbert2018-03-09
| |/ |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Previously [fun x : Ind@{i} => x : Ind@{j}] with Ind some cumulative inductive would try to generate a constraint [i = j] and use cumulativity only if this resulted in an inconsistency. This is confusingly different from the behaviour with [Type] and means cumulativity can only be used to lift between universes related by strict inequalities. (This isn't a kernel restriction so there might be some workaround to send the kernel the right constraints, but not in a nice way.) See modified test for more details of what is now possible. Technical notes: When universe constraints were inferred by comparing the shape of terms without reduction, cumulativity was not used and so too-strict equality constraints were generated. Then in order to use cumulativity we had to make this comparison fail to fall back to full conversion. When unifiying 2 instances of a cumulative inductive type, if there are any Irrelevant universes we try to unify them if they are flexible.
* | Merge PR #6747: Relax conversion of constructors according to the pCuIC modelGravatar Maxime Dénès2018-03-09
|\ \
* \ \ Merge PR #407: Fix SR breakage due to allowing fixpoints on non-rec valuesGravatar Maxime Dénès2018-03-09
|\ \ \
| * | | Fix SR breakage due to allowing fixpoints on non-rec valuesGravatar Matthieu Sozeau2018-03-08
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We limit fixpoints to Finite inductive types, so that BiFinite inductives (non-recursive records) are excluded from fixpoint construction. This is a regression in the sense that e.g. fixpoints on unit records were allowed before. Primitive records with eta-conversion are included in the BiFinite types. Fix deprecation Fix error message, the inductive type needs to be recursive for fix to work
| | * | Relax conversion of constructors according to the pCuIC modelGravatar Matthieu Sozeau2018-03-08
| |/ / |/| | | | | | | | | | | | | | - Nothing to check in conversion as they have a common supertype by typing. - In inference, enforce that one is lower than the other.
* | | Add empty description for @raise statements to satisfy ocamldocGravatar mrmr19932018-03-05
| | |
* | | Replace invalid tag @raises in ocamldoc comments with @raiseGravatar mrmr19932018-03-05
| | |
* | | Merge PR #6855: Update headers following #6543.Gravatar Maxime Dénès2018-03-05
|\ \ \
* \ \ \ Merge PR #935: Handling evars in the VMGravatar Maxime Dénès2018-03-04
|\ \ \ \
* \ \ \ \ Merge PR #6876: Unify Const_sorts and Const_type, and remove VsortGravatar Maxime Dénès2018-03-04
|\ \ \ \ \
| | | | | * Remove whd_both from the kernel.Gravatar Pierre-Marie Pédrot2018-03-04
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Now that the cache is distinct, there should be no nasty side-effects changing the value of one side while reducing the other.
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-25 10:31:37 +0000