aboutsummaryrefslogtreecommitdiff
path: root/kernel
AgeCommit message (Collapse)Author
2019-05-09Merge PR #10046: [primitive integers] Make div21 implems consistent with its ↵Maxime Dénès
specification Ack-by: Zimmi48 Ack-by: herbelin Ack-by: maximedenes Ack-by: proux01 Reviewed-by: vbgl
2019-05-03Remove now useless commented codePierre Roux
2019-05-03[primitive integers] Make div21 implems consistent with its specificationPierre Roux
There are three implementations of this primitive: * one in OCaml on 63 bits integer in kernel/uint63_amd64.ml * one in OCaml on Int64 in kernel/uint63_x86.ml * one in C on unsigned 64 bit integers in kernel/byterun/coq_uint63_native.h Its specification is the axiom `diveucl_21_spec` in theories/Numbers/Cyclic/Int63/Int63.v * comment the implementations with loop invariants to enable an easy pen&paper proof of correctness (note to reviewers: the one in uint63_amd64.ml might be the easiest to read) * make sure the three implementations are equivalent * fix the specification in Int63.v (only the lowest part of the result is actually returned) * make a little optimisation in div21 enabled by the proof of correctness (cmp is computed at the end of the first loop rather than at the beginning, potentially saving one loop iteration while remaining correct) * update the proofs in Int63.v and Cyclic63.v to take into account the new specifiation of div21 * add a test
2019-05-02Add union in Map interfaceMaxime Dénès
2019-04-30Merge PR #9952: Remove `constr_of_global_in_context`Pierre-Marie Pédrot
Reviewed-by: ppedrot
2019-04-29Merge PR #9925: [vm] Protect accu and coq_envMaxime Dénès
Ack-by: Zimmi48 Reviewed-by: maximedenes Ack-by: proux01 Reviewed-by: vbgl
2019-04-23Merge PR #9962: [native compiler] Encoding of constructors based on tagsPierre-Marie Pédrot
Ack-by: maximedenes Reviewed-by: ppedrot
2019-04-16[doc] [kernel] Add docstrings for native interface functions.Emilio Jesus Gallego Arias
2019-04-16Better error message when OCaml compiler not found for native computeMaxime Dénès
Fixes #6699
2019-04-15[vm] Protect accu and coq_envPierre Roux
Protect accu and coq_env against GC calls in the VM when calling primitive integer functions on 32 bits architecture.
2019-04-15[native compiler] Encoding of constructors based on tagsMaxime Dénès
This serves two purposes: 1. It makes the native compiler use the same encoding and lambda-representation as the bytecode compiler 2. It avoid relying on fragile invariants relating tags and constructor indices. For example, previously, the mapping from indices to tags had to be increasing.
2019-04-15[native compiler] Remove unused universe argument in LmakeblockMaxime Dénès
2019-04-15[native compiler] Distinguish constant constructors in lambda codeMaxime Dénès
2019-04-14[native compiler] Remove now unused GconstructMaxime Dénès
2019-04-14[native compiler] Remove `Lconstruct` from lambda code.Maxime Dénès
This is a step towards unifying the higher level ILs of the native and bytecode compilers. See https://github.com/coq/coq/projects/17
2019-04-12Remove `constr_of_global_in_context`Maxime Dénès
This function seems unused.
2019-04-05[native compiler] Fix critical bug with primitive projectionsMaxime Dénès
Since e1e7888, stuck projections were not computed correctly. Fixes #9684
2019-03-31Merge PR #9800: Less conv_tab allocations when pushing relevances, esp ↵Pierre-Marie Pédrot
skip_pattern Reviewed-by: ppedrot
2019-03-28[dune] Don't have `lib` depend on `dynlink`Emilio Jesus Gallego Arias
This is convenient for the bootstrap of `coqdep`
2019-03-22Merge PR #9602: [kernel] termination checking: backtrack on stuck case, fix, ↵Maxime Dénès
proj Ack-by: gares Reviewed-by: mattam82 Reviewed-by: maximedenes
2019-03-20Merge PR #9776: [kernel] Fix compare_head_gen_leq_with to use [leq] on ↵Gaëtan Gilbert
applications Reviewed-by: SkySkimmer
2019-03-18[kernel] Fix compare_head_gen_leq_with to use [leq] on applicationsMatthieu Sozeau
This fixes an incompleteness of subtyping on cumulative inductives, where I@{i} A <= I@{j} A should imply i <= j, i = j or no relation depending on the variance of I's universe.
2019-03-18Less conv_tab allocations when pushing relevances, esp skip_patternGaëtan Gilbert
2019-03-18Remove Term_typing.translate_mind indirectionGaëtan Gilbert
2019-03-18Merge PR #9740: Make NotConvertibleVect exception internal to typeopsPierre-Marie Pédrot
Reviewed-by: ppedrot
2019-03-14Put [@inline] on CClosure.Mark functionsGaëtan Gilbert
2019-03-14Switch order eqappr/check relevance in conversion.Gaëtan Gilbert
This takes advantage of the mutability of the fconstr relevance mark.
2019-03-14mutable relevance marks in fconstrGaëtan Gilbert
2019-03-14Repair relevance marks in-kernel.Gaëtan Gilbert
Prevent errors when under annotating binders.
2019-03-14Enable proof irrelevance for SProp.Gaëtan Gilbert
2019-03-14Inductives in SProp, forbid primitive records with only sprop fieldsGaëtan Gilbert
For nonsquashed: Either - 0 constructors - primitive record
2019-03-14Add relevance marks on binders.Gaëtan Gilbert
Kernel should be mostly correct, higher levels do random stuff at times.
2019-03-14Add a non-cumulative impredicative universe SProp.Gaëtan Gilbert
Note currently it's impossible to define inductives in SProp because indtypes.ml and the pretyper aren't fully plugged.
2019-03-14Make Sorts.t privateGaëtan Gilbert
2019-03-11Make NotConvertibleVect exception internal to typeopsGaëtan Gilbert
2019-03-11Nicer error for bad primitive types (through type_errors etc)Gaëtan Gilbert
2019-03-11Remove unused Retroknowledge.Register_inlineGaëtan Gilbert
This operation is done directly in Safe_typing.register_inline and has nothing to do with retroknowledge afaict.
2019-03-06Merge PR #9476: Constructor type information uses the expanded form.Gaëtan Gilbert
Reviewed-by: SkySkimmer Reviewed-by: gares
2019-03-01[Kernel] Simpler generation of opcode filesVincent Laporte
Files kernel/copcodes.ml, kernel/byterun/coq_instruct.h, and kernel/byterun/coq_jumptbl.h are generated by a simple OCaml program rather than a pipeline of sed and awk text processing.
2019-03-01write_uint63.ml: add headerVincent Laporte
2019-02-28Constructor type information uses the expanded form.Pierre-Marie Pédrot
It used to simply remember the normal form of the type of the constructor. This is somewhat problematic as this is ambiguous in presence of let-bindings. Rather, we store this data in a fully expanded way, relying on rel_contexts. Probably fixes a crapload of bugs with inductive types containing let-bindings, but it seems that not many were reported in the bugtracker.
2019-02-26Fix #9526: Registering inductives for primitive integers doesn't check enoughMaxime Dénès
2019-02-25[kernel] termination checking backtracks on stuck primitive projectionEnrico Tassi
2019-02-25[kernel] termination checking backtracks on stuck fixEnrico Tassi
2019-02-22[kernel] termination checking backtracks on stuck caseEnrico Tassi
The strategy is to backtrack when a constant is in head position: we first try to see if the arguments are guarded, if not we unfold. Since `Case` is represented as a head (rather than as a context as the reduction machine does) we did not backtrack there and reduce (including delta) the scrutinized in order to fire the iota redex. This commit adds a choice point in that specific case, and reduces eagerly (not step by step) the scrutinized in case of failure.
2019-02-17Separate variance and universe fields in inductives.Gaëtan Gilbert
I think the usage looks cleaner this way.
2019-02-11Fix #9527: unknown evar in nonterminating [fix] error.Gaëtan Gilbert
2019-02-08Remove global output_native_objects flag.Gaëtan Gilbert
2019-02-05Merge PR #9373: Kernel: don't automatically downgrade ill-shaped primitive ↵Pierre-Marie Pédrot
records Reviewed-by: ppedrot
2019-02-05Merge PR #9438: Cleanup universe length for inductives in vconvPierre-Marie Pédrot
Ack-by: SkySkimmer Reviewed-by: ppedrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-23 14:42:00 +0000