aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/cbytecodes.ml
Commit message (Collapse)AuthorAge
* Merge PR #7768: Fix #7723 (vm_compute segfault and proof of false)Gravatar Pierre-Marie Pédrot2018-06-27
|\
| * Fix #7723: vm_compute segfaults with universe polymorphismGravatar Maxime Dénès2018-06-27
| | | | | | | | Was revealing a critical bug in VM universe handling introduced in 8.5.
* | Remove Sorts.contentsGravatar Gaëtan Gilbert2018-06-26
|/
* [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.
* Less confusing debug printing of setfield bytecode instructionGravatar Maxime Dénès2018-05-28
|
* 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
|\ \
| * | 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.
| * Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
|/
* 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.
* 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.
* [api] Move structures deprecated in the API to the core.Gravatar Emilio Jesus Gallego Arias2017-11-06
| | | | We do up to `Term` which is the main bulk of the changes.
* [api] Deprecate all legacy uses of Names in core.Gravatar Emilio Jesus Gallego Arias2017-11-06
| | | | This will allow to merge back `Names` with `API.Names`
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
|
* Merge PR#189: Remove tabulation support from pretty-printing.Gravatar Maxime Dénès2017-02-20
|\
* \ Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-10-26
|\ \
| * | Fix #5127 Memory corruption with the VMGravatar Maxime Dénès2016-10-24
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The bytecode interpreter ensures that the stack space available at some points is above a static threshold. However, arbitrary large stack space can be needed between two check points, leading to segmentation faults in some cases. We track the use of stack space at compilation time and add an instruction to ensure greater stack capacity when required. This is inspired from OCaml's PR#339 and PR#7168. Patch written with Benjamin Grégoire.
* | | Use a better data structure for VM compilation of free vars.Gravatar Pierre-Marie Pédrot2016-08-22
| | | | | | | | | | | | This fixes #3450 and probably provides a huge speed-up to many instances.
| | * Remove tabulation support from pretty-printing.Gravatar Guillaume Melquiond2016-06-02
| |/ |/| | | | | | | | | | | | | This mechanism relied on functions that are deprecated in recent versions of ocaml. It was incorrectly used for the most part anyway. The only place that was using tabulations correctly is "print_loadpath", so there is a minor regression there: physical paths of short logical paths are no longer aligned.
* | Removing dead code and unused opens.Gravatar Pierre-Marie Pédrot2016-05-08
|/
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
|
* Refine Gregory Malecha's patch on VM and universe polymorphism.Gravatar Maxime Dénès2015-10-28
| | | | | | | | | | | | | | | | - Universes are now represented in the VM by a structured constant containing the global levels. This constant is applied to local level variables if any. - When reading back a universe, we perform the union of these levels and return a [Vsort]. - Fixed a bug: structured constants could contain local universe variables in constructor arguments, which has to be prevented. Was showing up for instance when evaluating [cons _ list (nil _)] with a polymorphic [list] type. - Fixed a bug: polymorphic inductive types can have an empty stack. Was showing up when evaluating [bool] with a polymorphic [bool] type. - Made a few cosmetic changes. Patch written with Benjamin Grégoire.
* Adds support for the virtual machine to perform reduction of universe ↵Gravatar Gregory Malecha2015-10-28
| | | | | | | | polymorphic definitions. - This implementation passes universes in separate arguments and does not eagerly instanitate polymorphic definitions. - This means that it pays no cost on monomorphic definitions.
* Gather VM tags in Cbytecodes.Gravatar Maxime Dénès2015-10-12
|
* print universes when dumping bytecode.Gravatar Gregory Malecha2015-09-03
|
* a small amount of documentation on the virtual machine.Gravatar Gregory Malecha2015-07-23
|
* Fix handling of primitive projections in VM.Gravatar Maxime Dénès2015-07-05
| | | | | I'm pushing this patch now because the previous treatment of such projections in the VM was already unsound. It should however be carefully reviewed.
* Add a Set Dump Bytecode command for debugging purposes.Gravatar Maxime Dénès2015-06-23
| | | | | Prints the VM bytecode produced by compilation of a constant or a call to vm_compute.
* use a more compact representation of non-constant constructorsGravatar Benjamin Gregoire2015-03-27
| | | | | | for which there corresponding tag are greater than max_variant_tag. The code is a merge with the patch proposed by Bruno on github barras/coq commit/504c753d7bb104ff4453fa0ede21c870ae2bb00c
* Fix bug 4157,Gravatar Benjamin Gregoire2015-03-26
| | | | | | | change the representation of inductive constructor when there is too many non constant constructors in the inductive type Conflicts: kernel/cbytegen.ml
* Correct restriction of vm_compute when handling universe polymorphicGravatar Matthieu Sozeau2015-01-15
| | | | | | | | | | definitions. Instead of failing with an anomaly when trying to do conversion or computation with the vm's, consider polymorphic constants as being opaque and keep instances around. This way the code is still correct but (obviously) incomplete for polymorphic definitions and we avoid introducing an anomaly. The patch does nothing clever, it only keeps around instances with constants/inductives and compile constant bodies only for non-polymorphic definitions.
* Update headers.Gravatar Maxime Dénès2015-01-12
|
* Modulification of identifierGravatar ppedrot2012-12-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16071 85f007b7-540e-0410-9357-904b9bb8a0f7
* fast bitwise operations (lor,land,lxor) on int31 and BigNGravatar letouzey2012-08-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15727 85f007b7-540e-0410-9357-904b9bb8a0f7
* Updating headers.Gravatar herbelin2012-08-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13323 85f007b7-540e-0410-9357-904b9bb8a0f7
* Removed $Id$ introduced inadvertently in r13005 (no more $Id$ since r12972)Gravatar herbelin2010-05-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13006 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added a few informations about file lineages (for the most part in kernel)Gravatar herbelin2010-05-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13005 85f007b7-540e-0410-9357-904b9bb8a0f7
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nettoyage de code en vue de la release. Plus de Warning: Unused Gravatar aspiwack2007-12-18
| | | | | | | | | Variable, et plus de trucs useless qui traînaient par ma faute (y compris dans le noyau, la honte). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10388 85f007b7-540e-0410-9357-904b9bb8a0f7
* ajout de head0 et tail0 en natifGravatar bgregoir2007-06-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9900 85f007b7-540e-0410-9357-904b9bb8a0f7
* Processor integers + Print assumption (see coqdev mailing list for the Gravatar aspiwack2007-05-11
| | | | | | | | | details). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9821 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Ajout d'un cast vm dans la syntaxe : x <: t Gravatar bgregoir2006-07-22
| | | | | | | | | | | | | | | | | | | Part contre ces cas sont detruis dans les "Definition" (pas dans les "Lemma") je comprends pas ou ils sont enlev'e... Si une id'ee ... - Correction d'un bug dans vm_compute plusieurs fois signal'e par Roland. - Meilleur compilation des coinductifs, on utilise maintenant vraimment du lazy. - Enfin un peu plus de doc dans le code de la vm. Benjamin git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9058 85f007b7-540e-0410-9357-904b9bb8a0f7
* IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name).Gravatar sacerdot2004-11-16
| | | | | | | | | | | | | | | MOVITATION: in a forthcoming commit the application of a substitution to a constant will return a constr and not a constant. The application of a substitution to a kernel_name will return a kernel_name. Thus "constant" should be use as a kernel name for references that can be delta-expanded. KNOWN PROBLEMS: the only problem faced is in pretyping/recordops.ml (the code that implements "Canonical Structure"s). The ADT is violated once in this ocaml module. My feeling is that the implementation of "Canonical Structure"s should be rewritten to avoid this situation. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6303 85f007b7-540e-0410-9357-904b9bb8a0f7
* Changement dans les boxed values .Gravatar gregoire2004-11-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6295 85f007b7-540e-0410-9357-904b9bb8a0f7
* COMMITED BYTECODE COMPILERGravatar barras2004-10-20
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6245 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-15 18:39:07 +0000