aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/byterun/coq_interp.c
Commit message (Collapse)AuthorAge
* 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.
* Make interpreter of PROJ simpler by not using the stack.Gravatar Guillaume Melquiond2015-10-14
|
* Remove some unused variables.Gravatar Guillaume Melquiond2015-10-14
|
* Fix some typos.Gravatar Guillaume Melquiond2015-10-14
|
* Fix a bug in 31 bit arithmetic, leading to failing conversion tests.Gravatar Maxime Dénès2015-09-06
| | | | | | | | | On 64 bits architectures, integers could have some of their 32 msb set to 1 internally in the VM. When read back to a Coq term, this was not observable. But an equality test would fail. From the user point of view, the symptom was that vm_compute; reflexivity would succeed but the subsequent Qed would fail. Bug reported by Tahina Ramananandro.
* Fixed critical bug in 31 bit arithmetic of VMGravatar Catalin Hritcu2015-09-06
| | | | ADDMULDIVINT31 was missing pops in some cases
* 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.
* Fix some ill-typed debugging code in the VM.Gravatar Guillaume Melquiond2015-04-27
|
* fix code and bound for SWITCH instruction.Gravatar Benjamin Gregoire2015-03-30
|
* allows the vm to deal with inductive type with 8388607 constant constructors ↵Gravatar Benjamin Gregoire2015-03-26
| | | | and 8388851 non-constant constructor.
* Fix compilation with forthcoming Ocaml version 4.03.Gravatar Arnaud Spiwack2015-03-13
| | | | | | | Backported from a patch for v8.4 by Pierre Chambart. Part of the commit has been rendered obsolete by code reorganisation, leaving: * OCaml runtime header files used to declare the int32, uint32, int64 and uint64 type. That got removed, and uses of those types should be replaced by the standard ones: uint32_t, int32_t, int64_t, uint64_t. Those are defined in stdint.h.
* Switch the few remaining iso-latin-1 files to utf8Gravatar Pierre Letouzey2014-12-09
|
* Remove some dead code in the vmGravatar letouzey2012-10-02
| | | | | | | | | | | | | Apparently Cysmtable.set_global_boxed is unused, and removing it allows to get rid of a bunch of C code concerning "boxed" things (including ACCUMULATECOND instruction). Still TODO: Csymtable.set_transparent_const and Csymtable.set_opaque_const appear to be no-ops. Should we remove them ? git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15845 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
* Fix thumb2-related build errorGravatar glondu2011-04-19
| | | | | | | | Bug-Debian: http://bugs.debian.org/cgi-bin/bugreport.cgi?bug=622882 Signed-off-by: Konstantinos Margaritis <markos@genesi-usa.com> Signed-off-by: Stephane Glondu <steph@glondu.net> git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14027 85f007b7-540e-0410-9357-904b9bb8a0f7
* CHANGES: a word about recent changes in coqide, about Ctrl-C in vmGravatar letouzey2011-04-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13948 85f007b7-540e-0410-9357-904b9bb8a0f7
* Checks for signals in VM, allowing it to be interrupted by Ctrl-C (experimental)Gravatar letouzey2011-04-01
| | | | | | | | | | | | | | | | | | We simply reuse the ocaml flag caml_signals_are_pending and the function caml_process_pending_signals, and place a test at some place of the interpreter loop (at a similar location as in ocaml byterun/interp.c). The symbols caml_* we use are not officially made public in *.h installed alongside ocaml, but they seem pretty stable (there since at least ocaml 3.10, independent of arch and of byte/asm), so we access them via "extern". For once, thanks dirty C... In addition to that, when catching a Ctrl-C, we reset the vm via "coq_sp = coq_stack_high" as suggested by Benjamin G. This patch should be quite portable, it might even work in win32. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13947 85f007b7-540e-0410-9357-904b9bb8a0f7
* Discontinue support for ocaml 3.09.*Gravatar letouzey2010-05-19
| | | | | | Ocaml 3.10.0 is already three year old... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13015 85f007b7-540e-0410-9357-904b9bb8a0f7
* Rely on ocamlc to call the C compiler...Gravatar glondu2008-09-04
| | | | | | | | | | | ...with proper options for dynamic loading of C stubs. I believe this is the preferred way of compiling C stubs. It also adds by itself -fno-defer-pop, -Wall, -I `ocamlc -where`, so CFLAGS could also be simplified. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11358 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction du problème de complexité de Print Assumptions :Gravatar aspiwack2008-05-27
| | | | | | | | | | | | | | | | | | | | - Suite à une modification faite maladroitement, on ne se contentait pas de comparer le nom de la supposition quand on l'insérait dans l'ensemble des suppositions utilisées, mais aussi son type, ce qui était inutilement long (mais pas le facteur principal) - L'environnement était parcouru deux fois pour chaque variable de section. Ce n'était pas très grave vu qu'en général on a assez peu de variables de sections sous la main. Mais ça restait inutile. - Les noms qui ont déjà étés explorés sont maintenant memoizés, ce qui gagne dans le cas les pires (comme les théorèmes sur les réels typiquement) une exponentiel dans le temps de recherche (si on visualise l'espace de recherche comme un DAG, l'ancienne procédure le parcourais comme si il était un arbre, ce qui a une complexité exponentielle en la taille du DAG). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11001 85f007b7-540e-0410-9357-904b9bb8a0f7
* patch for C code of addmuldiv31Gravatar thery2008-02-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10593 85f007b7-540e-0410-9357-904b9bb8a0f7
* * Adding compability with ocaml 3.10 + camlp5 (rework of Gravatar letouzey2007-09-15
| | | | | | | | | | | | | | the patch by S. Mimram) * for detecting architecture, also look for /bin/uname * restore the compatibility of kernel/byterun/coq_interp.c with ocaml 3.07 (caml_modify vs. modify). There is still an issue with this 3.07 and 64-bits architecture (see coqdev and a future bug report). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10122 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
* corrections bug dans l'implem de int31Gravatar bgregoir2007-05-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9822 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
* Changement dans le kernel : Gravatar bgregoir2006-12-11
| | | | | | | | | | | | | | | | | | | | | - essai de suppression des dependances debiles. (echec) - Application des patch debian. Pour ring et field : - introduciton de la function de sign et de puissance. - Correction de certains bug. - supression de ring_replace .... Pour exact_no_check : - ajout de la tactic : vm_cast_no_check (t) qui remplace "exact_no_check (t<: type of Goal)" (cette version forcais l'evaluation du cast dans le pretypage). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9427 85f007b7-540e-0410-9357-904b9bb8a0f7
* changement des _sym par _comm dans setoid_ringGravatar bgregoir2006-10-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9299 85f007b7-540e-0410-9357-904b9bb8a0f7
* Appel à caml_modify pour Ocaml 3.07Gravatar notin2006-09-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9102 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modifications dans les scripts de configuration (coqtop et coqide affichent ↵Gravatar notin2006-07-28
| | | | | | maintenant le numéro de révision svn) + correction problème OCaml 3.07 et caml_;odify git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9063 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
* Changement des named_contextGravatar gregoire2005-12-02
| | | | | | | | Ajout de cast indiquant au kernel la strategie a suivre Resolution du bug sur les coinductifs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7639 85f007b7-540e-0410-9357-904b9bb8a0f7
* compatibility with POWERPCGravatar gregoire2004-11-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6338 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-06-30 06:55:35 +0000