aboutsummaryrefslogtreecommitdiff
path: root/kernel/nativecode.ml
AgeCommit message (Collapse)Author
2013-10-24More monomorphic List.mem + List.assoc + ...letouzey
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
2013-10-24Specializing hash functions for widely used types.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16933 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-24Turn many List.assoc into List.assoc_fletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16925 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-27Removing a bunch of generic equalities.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16806 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-07-06Fixing a bug in the native compiler, introduced by r16363, leading to undefinedmdenes
variables in the generated code. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16619 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-04-29Merging Context and Sign.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16463 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-04-29Splitting Term into five unrelated interfaces:ppedrot
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
2013-03-25Native compiler: hash-consing of generated code and values.mdenes
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16363 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-25Native compiler: Inlined constants are now compiled, fixing a bug reported bymdenes
Chantal Keller. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16356 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-13Restrict (try...with...) to avoid catching critical exn (part 8)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16284 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-12invalid_arg instead of raise (Invalid_argement ...)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16270 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-05More monomorphization.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16260 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-02-26kernel/declarations becomes a pure mliletouzey
- 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
2013-02-26Names: shortcuts for building {kn, constant, mind} with empty sectionsletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16249 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-02-18use List.rev_map whenever possibleletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16211 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-02-11Fixing bug in native compiler with let patterns in fixpoint definitions.mdenes
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
2013-01-28Uniformization of the "anomaly" command.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16165 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-01-28native_compute: Fixed dependencies compilation order.mdenes
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16162 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-01-22New implementation of the conversion test, using normalization by evaluation tomdenes
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.25.1) at 2026-02-01 08:24:51 +0000