aboutsummaryrefslogtreecommitdiff
path: root/kernel
AgeCommit message (Collapse)Author
2018-09-03Merge PR #8124: Fix #8121: anomalies in native_compute with let and evars.Maxime Dénès
2018-09-03Merge PR #7953: More efficient abstraction over variables in Cooking.Maxime Dénès
2018-09-03Merge PR #7912: Simplify effects APIMaxime Dénès
2018-07-26Fix #8121: anomalies in native_compute with let and evars.Pierre-Marie Pédrot
Même causes, mêmes effets, similar fix to #8119: - Do not pass let-bound arguments to evars. We seize the opportunity to remove the useless type information for Aevar. Special fixes to native compilation: - Evars are not handled correctly when iterating over lambda terms. - Names.id_of_string is gone. - Evar instances are not reified in the right order.
2018-07-26Turn the kernel reduction sharing flag into an argument passed in the cache.Pierre-Marie Pédrot
We move the global declaration of that argument to the environment, and reuse the Global module to handle this flag. Note that the checker was not using this flag before this patch, and still doesn't use it. This should probably be fixed in a later patch.
2018-07-26Merge PR #8122: Fix #8119: anomalies in vm_compute with let and evars.Maxime Dénès
2018-07-26Merge PR #8084: Properly disable native compilation when -native-compiler is ↵Maxime Dénès
unset.
2018-07-24Fix #8119: anomalies in vm_compute with let and evars.Pierre-Marie Pédrot
There were actually two broken things with VM + evars, the fixes are: - Do not pass let-bound arguments to evars. - Use the right order for evar arguments. Native compilation seems to be suffering from the same shortcomings, I will open a separate bug and adapt the PR.
2018-07-24Add combinators to drop the bodies of local declarations.Pierre-Marie Pédrot
2018-07-24Properly disable native compilation when -native-compiler is unset.Pierre-Marie Pédrot
There was a function used by the pretyper that did not check that the flag was set, leading to native compilation even when the configure flag was off.
2018-07-24VM: don't duplicate projection narg information in lproj/kprojGaëtan Gilbert
2018-07-24Projections use index representationGaëtan Gilbert
The upper layers still need a mapping constant -> projection, which is provided by Recordops.
2018-07-24Merge PR #8000: Fix #7854: Native compilation + flambda trigger SEGFAULT.Maxime Dénès
2018-07-17Merge PR #8055: Fast accumulator check in native compilationMaxime Dénès
2018-07-14[ltac] Remove unused functions / constructors.Emilio Jesus Gallego Arias
Catched by compiling the ml files from ml4.
2018-07-13Generate type-specific code for is_accu in native compilation of fixpoints.Pierre-Marie Pédrot
This is much more efficient than using Nativevalues.is_accu function which incurs a lot of irrelevant checks on its argument.
2018-07-13Store the {struct} inductive type in native fixpoint AST.Pierre-Marie Pédrot
2018-07-13Pass a proper environment to Nativelambda.lambda_of_constr.Pierre-Marie Pédrot
No need to roll up a new data structure when Environment has O(log n) add and lookup of rel definitions.
2018-07-12Fix #7854: Native compilation + flambda trigger SEGFAULT.Pierre-Marie Pédrot
We use a more abstract representation for accumulators in the native compilation scheme, that requires less fiddling with low-level implementation details. It might be slower though.
2018-07-03Term_typing: remove unused argument to internal function.Gaëtan Gilbert
The function is defined with a typo but called with the same env that is mistakenly not shadowed. An alternative to this commit would be to fix the typo.
2018-07-03Cooking.cook_constant: remove unused env argument.Gaëtan Gilbert
Unused since d95306323 (remove template polymorphic definitions).
2018-07-03Indtypes: remove unused is_unit.Gaëtan Gilbert
2018-07-03Subtyping.check_constant: remove unused module path argument.Gaëtan Gilbert
2018-07-03Inductive.extract_stack,filter_stack_domain: remove unused argumentsGaëtan Gilbert
2018-07-03Nativecode compile_mind, compile_mind_field: remove unused argumentsGaëtan Gilbert
2018-07-03Nativecode.pp_mllam internal pp_letrec: remove unused argument.Gaëtan Gilbert
2018-07-03Modops.add_retroknowledge: remove unused argument.Gaëtan Gilbert
Unused since fe1979bf47951352ce32a6709cb5138fd26f311d. I'm not sure if it was actually used back then since I didn't look at the function it was passed to.
2018-06-29Merge PR #7080: Swapping Context and Constr and defining declarations on ↵Maxime Dénès
constr in Constr
2018-06-29More efficient abstraction over variables in Cooking.Pierre-Marie Pédrot
Instead of repeatedly replacing the variables with a De Bruijn index and closing it, we do this in one pass. We furthermore share the abstraction over the context. This source of slowdown was observed in lambda-rust.
2018-06-28Deprecate Environ.retroknowledge function in favor of the projectionGaëtan Gilbert
2018-06-28[env.env_rel_context.env_rel_ctx] -> [rel_context env]Gaëtan Gilbert
It's a bit shorter and more direct.
2018-06-28Make Environ.globals abstract.Gaëtan Gilbert
2018-06-27Merge PR #7768: Fix #7723 (vm_compute segfault and proof of false)Pierre-Marie Pédrot
2018-06-27Swapping Context and Constr: defining declarations on constr in Constr.Hugo Herbelin
This shall eventually allow to use contexts of declarations in the definition of the "Case" constructor. Basically, this means that Constr now includes Context and that the "t" types of Context which were specialized on constr are not defined in Constr (unfortunately using a heavy boilerplate).
2018-06-27Merge PR #7863: Remove Sorts.contentsPierre-Marie Pédrot
2018-06-27Test file for #7723Maxime Dénès
2018-06-27Fix #7723: vm_compute segfaults with universe polymorphismMaxime Dénès
Was revealing a critical bug in VM universe handling introduced in 8.5.
2018-06-26Merge PR #7919: Fix equality check on global names from native compute.Maxime Dénès
2018-06-26Remove Sorts.contentsGaëtan Gilbert
2018-06-25Merge PR #7798: Remove hack skipping comparison of algebraic universes in ↵Matthieu Sozeau
subtyping.
2018-06-25Fix equality check on global names from native compute.Pierre-Marie Pédrot
Not sure it could have led to a soundness bug, but this is definitely serious enough to deserve a backport. Also made the code robust by listing all the constructors.
2018-06-24Further cleaning of the side-effect API.Pierre-Marie Pédrot
We remove internal functions and types from the API.
2018-06-24Share the role type between the implementations of side-effects.Pierre-Marie Pédrot
We simply exploit a type isomorphism to remove the use of dedicated algebraic types in the kernel which are actually not necessary.
2018-06-24Merge PR #7772: [native_compute] Delay computations with toplevel matchPierre-Marie Pédrot
2018-06-23Merge PR #7614: Simplify the code that handles trust of side-effects in ↵Maxime Dénès
kernel typing.
2018-06-23Adapt the kernel to generate proper data for mutual records.Pierre-Marie Pédrot
Upper layers are still not able to handle mutual records though.
2018-06-23Using more general information for primitive records.Pierre-Marie Pédrot
This brings more compatibility with handling of mutual primitive records in the kernel.
2018-06-23Change the proj_ind field from MutInd.t to inductive.Pierre-Marie Pédrot
This is a first step towards the acceptance of mutual record types in the kernel.
2018-06-23Merge PR #7715: Simplify the cooking of primitive projections.Maxime Dénès
2018-06-22Merge PR #7600: Faster and cleaner fconstr-to-constr conversion function.Maxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-26 17:38:31 +0000