aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel
Commit message (Collapse)AuthorAge
* [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.
* 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.
| | | | | * Pass the constant cache as a separate argument in kernel reduction.Gravatar Pierre-Marie Pédrot2018-03-04
| | | | | |
| | * | | | Handling evars in the VM.Gravatar Pierre-Marie Pédrot2018-03-03
| | | |_|/ | | |/| | | | | | | | | | | | | | | | | | | | | | | | | | | We simply treat them as as an application of an atom to its instance, and in the decompilation phase we reconstruct the instance from the stack. This grants wish BZ#5659.
| * / | | [VM] Unify Const_sorts and Const_type, and remove Vsort.Gravatar Maxime Dénès2018-03-02
| |/ / / | | | | | | | | | | | | | | | | This simplifies the representation of values, and brings it closer to the ones of the native compiler.
* / / / Fix #6878: univ undefined for [with Definition] bad instance size.Gravatar Gaëtan Gilbert2018-03-01
|/ / /
* | | Merge PR #6734: dest_{prod,lam}: no Cast case (it's removed by whd)Gravatar Maxime Dénès2018-02-28
|\ \ \ | |_|/ |/| |
| | * Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
| |/ |/|
* | Merge PR #6784: New IR in VM: ClambdaGravatar Maxime Dénès2018-02-24
|\ \
| * | New IR in VM: Clambda.Gravatar Maxime Dénès2018-02-23
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This intermediate representation serves two purposes: 1- It is a preliminary step for primitive machine integers, as iterators will be compiled to Clambda. 2- It makes the VM compilation passes closer to the ones of native_compute. Once we unifiy the representation of values, we should be able to factorize the lambda-code generation between the two compilers, as well as the reification code. This code was written by Benjamin Grégoire and myself.
| * | Fix map iterator on nativelambda.Gravatar Maxime Dénès2018-02-23
| | |
* | | Merge PR #6740: Adding a sanity check on inductive variance subtyping.Gravatar Maxime Dénès2018-02-21
|\ \ \ | |/ / |/| |
* | | Merge PR #6728: Extrude monomorphic universe contexts from with Definition ↵Gravatar Maxime Dénès2018-02-19
|\ \ \ | | | | | | | | | | | | constraints.
| * | | Extrude monomorphic universe contexts from with Definition constraints.Gravatar Pierre-Marie Pédrot2018-02-16
| | | | | | | | | | | | | | | | | | | | We defer the computation of the universe quantification to the upper layer, outside of the kernel.
| | * | Adding a sanity check on inductive variance subtyping.Gravatar Pierre-Marie Pédrot2018-02-15
| |/ /
* | | Factorize the relocations in the on-disk VM representation.Gravatar Pierre-Marie Pédrot2018-02-14
| | | | | | | | | | | | | | | Instead of using a linear representation, we simply use a table that maps every kind of relocation to the list of positions it needs to be applied to.
* | | Use a more compact representation for bytecode relocations stored on disk.Gravatar Pierre-Marie Pédrot2018-02-14
| | | | | | | | | | | | | | | | | | | | | | | | | | | The previous implementation used a list of pairs, which has size 9n where n is the number of relocations. We instead use two arrays for a total memory cost of 2n + 5 words. The use of arrays may turn out to be problematic on 32-bit machines, I am unsure if we will hit this limitation in practice.
* | | Do not use global variables for VM bytecode compilation in Cemitcodes.Gravatar Pierre-Marie Pédrot2018-02-14
| | | | | | | | | | | | Instead we thread a buffer.
* | | Remove the unsafe bytes conversion function in Cemitcodes.Gravatar Pierre-Marie Pédrot2018-02-14
| | | | | | | | | | | | | | | This is actually not needed, as the only thing we do with this Bytes.t is to pass it to a C function which will use it in a read-only way.
* | | Move the call to the computation of bytecode inside Cemitcodes.Gravatar Pierre-Marie Pédrot2018-02-14
| | | | | | | | | | | | | | | This shouldn't matter because the tcode_of_code function is pure, its only effect being allocating a string and filling it with the translated bytecode.
* | | Abstract further the type of VM bytecode compilation.Gravatar Pierre-Marie Pédrot2018-02-14
|/ / | | | | | | This reduces the possibility to wreak havoc while making the API nicer.
* | Merge PR #6713: Fix #6677: Critical bug with VM and universesGravatar Maxime Dénès2018-02-14
|\ \
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-20 23:17:03 +0000