aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/nativecode.ml
Commit message (Collapse)AuthorAge
...
* Fixing ml-doc.Gravatar Pierre-Marie Pédrot2014-05-01
|
* Fix exponential behavior in native compiler with retroknowledge.Gravatar Maxime Dénès2014-04-09
|
* Optimizing Int31 support in native compiler, by not taggingGravatar Maxime Dénès2014-04-09
| | | | applications of I31 constructor as lazy.
* Machine arithmetic operations for native compiler.Gravatar Maxime Dénès2014-04-09
| | | | | This completes the port of the native compiler to retroknowledge. However, some testing and optimizations are still to be done.
* Full support for int31 values in native compiler.Gravatar Maxime Dénès2014-04-09
|
* Partial support for open terms in int31.Gravatar Maxime Dénès2014-04-09
|
* Had to split Nativelambda in two files because of RetroknowledgeGravatar Maxime Dénès2014-04-09
| | | | dependencies.
* Int31 literals in native compiler.Gravatar Maxime Dénès2014-04-09
|
* Fixing generic hashes and replacing them with proper ones.Gravatar Pierre-Marie Pédrot2014-03-03
|
* Hunting pervasive equality in native compiler. It seems they were used forGravatar Pierre-Marie Pédrot2014-03-01
| | | | | optimization purposes. I replaced their use with the under-approximation of pointer equality.
* Lazyconstr -> OpaqueproofGravatar Enrico Tassi2014-02-26
| | | | | Make this module deal only with opaque proofs. Make discharging/substitution invariant more explicit via a third constructor.
* Support for evars and metas in native compiler.Gravatar Maxime Dénès2013-12-30
| | | | | | | | | | | | | | | | Experimental. Turned out to be much harder to implement than I thought. The main issue is that the reification in the native compiler and the VM is not quite untyped. Indeed, type annotations for lambdas have to be reconstructed. Hence, when reifying an application u = t a1 ... an, the type of t has to be known or reconstructed. It is always possible to do so in plain CIC, when u is in normal form and its type is known. However, with partial terms this may no longer be the case, as in: ?1 a1 ... an. So we also compile and evaluate the type of evars and metas. This still has to be tested more extensively, but the correction of the kernel native conversion (on terms without evars or metas) should not be impacted. Much of this could be reused for the VM.
* Got rid of unused lazy flag in the native compiler.Gravatar Maxime Dénès2013-12-29
|
* Removing native_name reference from constant_body.Gravatar Maxime Dénès2013-12-28
| | | | | | For now, this reference (renamed to link_info) has been moved to the environment (for constants and inductive types). But this is only a first step towards making the native compiler more functional.
* More monomorphic List.mem + List.assoc + ...Gravatar letouzey2013-10-24
| | | | | | | | | | | To reduce the amount of syntactic noise, we now provide a few inner modules Int.List, Id.List, String.List, Sorts.List which contain some monomorphic (or semi-monomorphic) functions such as mem, assoc, ... NB: for Int.List.mem and co we reuse List.memq and so on. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16936 85f007b7-540e-0410-9357-904b9bb8a0f7
* Specializing hash functions for widely used types.Gravatar ppedrot2013-10-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16933 85f007b7-540e-0410-9357-904b9bb8a0f7
* Turn many List.assoc into List.assoc_fGravatar letouzey2013-10-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16925 85f007b7-540e-0410-9357-904b9bb8a0f7
* Removing a bunch of generic equalities.Gravatar ppedrot2013-09-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16806 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing a bug in the native compiler, introduced by r16363, leading to undefinedGravatar mdenes2013-07-06
| | | | | | | variables in the generated code. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16619 85f007b7-540e-0410-9357-904b9bb8a0f7
* Merging Context and Sign.Gravatar ppedrot2013-04-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16463 85f007b7-540e-0410-9357-904b9bb8a0f7
* Splitting Term into five unrelated interfaces:Gravatar ppedrot2013-04-29
| | | | | | | | | | | | | | | | | 1. sorts.ml: A small file utility for sorts; 2. constr.ml: Really low-level terms, essentially kind_of_constr, smart constructor and basic operators; 3. vars.ml: Everything related to term variables, that is, occurences and substitution; 4. context.ml: Rel/Named context and all that; 5. term.ml: derived utility operations on terms; also includes constr.ml up to some renaming, and acts as a compatibility layer, to be deprecated. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16462 85f007b7-540e-0410-9357-904b9bb8a0f7
* Native compiler: hash-consing of generated code and values.Gravatar mdenes2013-03-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16363 85f007b7-540e-0410-9357-904b9bb8a0f7
* Native compiler: Inlined constants are now compiled, fixing a bug reported byGravatar mdenes2013-03-25
| | | | | | | Chantal Keller. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16356 85f007b7-540e-0410-9357-904b9bb8a0f7
* Restrict (try...with...) to avoid catching critical exn (part 8)Gravatar letouzey2013-03-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16284 85f007b7-540e-0410-9357-904b9bb8a0f7
* invalid_arg instead of raise (Invalid_argement ...)Gravatar letouzey2013-03-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16270 85f007b7-540e-0410-9357-904b9bb8a0f7
* More monomorphization.Gravatar ppedrot2013-03-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16260 85f007b7-540e-0410-9357-904b9bb8a0f7
* kernel/declarations becomes a pure mliGravatar letouzey2013-02-26
| | | | | | | | - constr_substituted and lazy_constr are now in a dedicated kernel/lazyconstr.ml - the functions that were in declarations.ml (mostly substitution utilities and hashcons) are now in kernel/declareops.ml git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16250 85f007b7-540e-0410-9357-904b9bb8a0f7
* Names: shortcuts for building {kn, constant, mind} with empty sectionsGravatar letouzey2013-02-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16249 85f007b7-540e-0410-9357-904b9bb8a0f7
* use List.rev_map whenever possibleGravatar letouzey2013-02-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16211 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing bug in native compiler with let patterns in fixpoint definitions.Gravatar mdenes2013-02-11
| | | | | | | | | | Typical example: Fixpoint f (m : nat) (o := true) (n : nat) {struct n} := n. Was raising an "index out of bounds" exception at compile-time. Nota: this construction is still incorrectly handled by the VM. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16197 85f007b7-540e-0410-9357-904b9bb8a0f7
* Uniformization of the "anomaly" command.Gravatar ppedrot2013-01-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16165 85f007b7-540e-0410-9357-904b9bb8a0f7
* native_compute: Fixed dependencies compilation order.Gravatar mdenes2013-01-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16162 85f007b7-540e-0410-9357-904b9bb8a0f7
* New implementation of the conversion test, using normalization by evaluation toGravatar mdenes2013-01-22
native OCaml code. Warning: the "retroknowledge" mechanism has not been ported to the native compiler, because integers and persistent arrays will ultimately be defined as primitive constructions. Until then, computation on numbers may be faster using the VM, since it takes advantage of machine integers. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16136 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-30 16:55:47 +0000