aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel
Commit message (Collapse)AuthorAge
* Merge PR #6734: dest_{prod,lam}: no Cast case (it's removed by whd)Gravatar Maxime Dénès2018-02-28
|\
* \ 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
|\ \
* \ \ Merge PR #6702: [vernac] [minor] Move print effects to top-level caller.Gravatar Maxime Dénès2018-02-13
|\ \ \
* \ \ \ Merge PR #1082: Fixing Print for inductive types with let-in in parametersGravatar Maxime Dénès2018-02-12
|\ \ \ \
* \ \ \ \ Merge PR #6128: Simplification: cumulativity information is variance ↵Gravatar Maxime Dénès2018-02-12
|\ \ \ \ \ | | | | | | | | | | | | | | | | | | information.
* \ \ \ \ \ Merge PR #6729: [nativecomp] Remove ad-hoc handling of Dynlink exception.Gravatar Maxime Dénès2018-02-12
|\ \ \ \ \ \
* \ \ \ \ \ \ Merge PR #6674: Delay computation of lifts in the reduction machine.Gravatar Maxime Dénès2018-02-12
|\ \ \ \ \ \ \
| | | | | | * | Fix #6677: Critical bug with VM and universesGravatar Maxime Dénès2018-02-12
| |_|_|_|_|/ / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This bug was present since the first patch adding universe polymorphism handling in the VM (Coq 8.5). Note that unsoundness can probably be observed even without universe polymorphism.
| | | * | | | Universe instance printer: add optional variance argument.Gravatar Gaëtan Gilbert2018-02-11
| | | | | | |
| | | * | | | Use specialized function for inductive subtyping inference.Gravatar Gaëtan Gilbert2018-02-11
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This ensures by construction that we never infer constraints outside the variance model.
| | | | | | * dest_{prod,lam}: no Cast case (it's removed by whd)Gravatar Gaëtan Gilbert2018-02-11
| |_|_|_|_|/ |/| | | | |
| | | * | | Simplification: cumulativity information is variance information.Gravatar Gaëtan Gilbert2018-02-10
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Since cumulativity of an inductive type is the universe constraints which make a term convertible with its universe-renamed copy, the only constraints we can get are between a universe and its copy. As such we do not need to be able to represent arbitrary constraints between universes and copied universes in a double-sized ucontext, instead we can just keep around an array describing whether a bound universe is covariant, invariant or irrelevant (CIC has no contravariant conversion rule). Printing is fairly obtuse and should be improved: when we print the CumulativityInfo we add marks to the universes of the instance: = for invariant, + for covariant and * for irrelevant. ie Record Foo@{i j k} := { foo : Type@{i} -> Type@{j} }. Print Foo. gives Cumulative Record Foo : Type@{max(i+1, j+1)} := Build_Foo { foo : Type@{i} -> Type@{j} } (* =i +j *k |= *)
| | | * | | [get_cumulativity_constraints] allowing further code sharing.Gravatar Gaëtan Gilbert2018-02-10
| | | | | |
| | | * | | Factorize code for comparing maybe-cumulative inductives.Gravatar Gaëtan Gilbert2018-02-10
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The part in Reduction should be semantics preserving, but Reductionops only tried cumulativity if equality fails. This is probably wrong so I changed it.
| | | * | | Fix typo in Univ.CumulativityInfoGravatar Gaëtan Gilbert2018-02-10
| |_|/ / / |/| | | |
| | | | * [nit] Remove some unnecessary global `open Feedback`Gravatar Emilio Jesus Gallego Arias2018-02-09
| | | |/ | | |/|
| | * | [nativecomp] Remove ad-hoc handling of Dynlink exception.Gravatar Emilio Jesus Gallego Arias2018-02-09
| |/ / |/| | | | | | | | | | | Instead, we properly register a printer for such exception and update the code.
* | | Merge PR #6685: Use whd-all on rigid-flex conversion.Gravatar Maxime Dénès2018-02-07
|\ \ \
* \ \ \ Merge PR #6686: Kernel/checker reduction cleanups around projection unfoldingGravatar Maxime Dénès2018-02-07
|\ \ \ \
| | * | | Respect the transparent state of the current conversion on strong weak-head.Gravatar Pierre-Marie Pédrot2018-02-05
| | | | | | | | | | | | | | | | | | | | | | | | | This fixes the previous patch in rare corner-cases where unification code was relying on both kernel conversion and specific transparent state.
* | | | | [native_compute] Fix handling of evars in conversionGravatar Maxime Dénès2018-02-05
| | | | |
* | | | | [native_compute] Remove useless conversion to list in reification.Gravatar Maxime Dénès2018-02-05
| | | | |
| | | * | Delay computation of lifts in the reduction machine.Gravatar Pierre-Marie Pédrot2018-02-04
| |_|/ / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | This definitely qualifies as a micro-optimization, but it would not be performed by Flambda. Indeed, it is unsound in general w.r.t. OCaml semantics, as it involves a fixpoint and changes potential non-termination. In our case it doesn't matter semantically, but it is indeed observable on computation intensive developments like UniMath.
| * | | CClosure.unfold_projection: don't catch Not_found, assume env is okGravatar Gaëtan Gilbert2018-02-02
| | | | | | | | | | | | | | | | | | | | We can do this after the parent commit (Reductionops.nf_* don't use empty env)
| * | | kernel: cleanup projection unfoldingGravatar Gaëtan Gilbert2018-02-02
|/ / / | | | | | | | | | | | | - use Redflags.red_projection - share unfold_projection between CClosure and Reduction
| * / Use whd-all on rigid-flex conversion.Gravatar Pierre-Marie Pédrot2018-02-02
|/ / | | | | | | | | | | | | | | | | | | | | | | | | This heuristic is justified by the fact that during a conversion check between a flexible and a rigid term, the flexible one is eventually going to be fully weak-head normalized. So in this case instead of performing many small reduction steps on the flexible term, we perform full weak-head reduction, including delta. It is slightly more efficient in actual developments, and it fixes a corner case encountered by Jason Gross. Fixes #6667: Kernel conversion is much, much slower than `Eval lazy`.
* | Merge PR #6666: Fix reduction of primitive projections on coinductive ↵Gravatar Maxime Dénès2018-01-30
|\ \ | | | | | | | | | records for cbv and native_compute
* \ \ Merge PR #6649: Fix #6621: Anomaly on fixpoint with primitive projectionsGravatar Maxime Dénès2018-01-30
|\ \ \
| | * | [native_compute] Fix evaluation of cofixpoints under primitive projections.Gravatar Maxime Dénès2018-01-29
| | | |
* | | | Safer VM interfacesGravatar Maxime Dénès2018-01-26
| |/ / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We separate functions dealing with VM values (vmvalues.ml) and interfaces of the bytecode interpreter (vm.ml). Only the former relies on untyped constructions. This also makes the VM architecture closer to the one of native_compute, another patch could probably try to share more code between the two for conversion and reification (not trivial, though). This is also preliminary work for integers and arrays.
| * | Fix #6621: Anomaly on fixpoint with primitive projectionsGravatar Maxime Dénès2018-01-24
|/ / | | | | | | | | | | | | | | The implementation of the subterm relation for primitive projections was a bit wrong. I found the problem independently of this bug, and tried to see if a proof of False could be derived, but I don't think so, due to another check (check_is_subterm) that saves the kernel at the last minute.
* | Merge PR #6627: Fix #6619: coqchk does not reduce compatibility constants ↵Gravatar Maxime Dénès2018-01-23
|\ \ | | | | | | | | | for primitive projections
* \ \ Merge PR #6506: Fast rel lookupGravatar Maxime Dénès2018-01-22
|\ \ \
| | * | Remove dead code in Environ.Gravatar Pierre-Marie Pédrot2018-01-20
| |/ / |/| | | | | | | | | | | | | | | | | The constant_value function was actually not behaving the same as constant_value_in w.r.t. projections. The former was not used, and the only place that used the latter was in Tacred and was statically insensitive to the use of projections.
* | | Store the conversion oracle in constant and inductive definitions.Gravatar Pierre-Marie Pédrot2018-01-14
| | | | | | | | | | | | | | | We also have to update the checker to deserialize this additional data, but it is not using it in type-checking yet.
* | | Merge PR #6578: Remove references to deleted Unicode.Unsupported exceptionGravatar Maxime Dénès2018-01-13
|\ \ \
* | | | Enforce that polymorphic definitions do not generate internal constraints.Gravatar Pierre-Marie Pédrot2018-01-11
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | In practice, we only send to the kernel polymorphic definitions whose side-effects have been exported first, and furthermore their bodies have already been forced. Therefore, no constraints are generated by the kernel. Nonetheless, it might be desirable in the future to also defer computation of polymorphic proofs whose constraints have been explicited in the type. It is not clear when this is going to be implemented. Nonetheless, the current check is not too drastic as it only prevents monomorphic side-effects to appear inside polymorphic opaque definitions. The only way I know of to trigger such a situation is to generate a scheme in a proof, as even abstract is actually preserving the polymorphism status of the surrounding proof. It would be possible to work around such rare instances anyways. As for internal constraints generated by a potentially deferred polymorphic body, it is easy to check that they are a subset of the exported ones at a higher level inside the future computation and fail there. So in practice this patch is not too restrictive and it highlights a rather strong invariant of the kernel code.
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-28 15:53:50 +0000