aboutsummaryrefslogtreecommitdiff
path: root/kernel
AgeCommit message (Collapse)Author
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
2018-06-22Remove hack skipping comparison of algebraic universes in subtyping.Gaëtan Gilbert
When inferring [u <= v+k] I replaced the exception and instead add [u <= v]. This is trivially sound and it doesn't seem possible to have the one without the other (except specially for [Set <= v+k] which was already handled). I don't know an example where this used to fail and now succeeds (the point was to remove an anomaly, but the example ~~~ Module Type SG. Definition DG := Type. End SG. Module MG : SG. Definition DG := Type : Type. Fail End MG. ~~~ now fails with universe inconsistency. Fix #7695 (soundness bug!).
2018-06-22Define and use UGraph.enforce_leq_alg for subtyping inferenceGaëtan Gilbert
Not sure if worth using in other places.
2018-06-19Fix Univ.enforce_leq dropped constraints when algebraic on the rightGaëtan Gilbert
There's probably a proof of false using subtyping if someone wants to look. NB: the checker doesn't handle algebraics on the right.
2018-06-19Merge PR #7841: Remove CanaryPierre-Marie Pédrot
2018-06-18Remove Canary.whitequark
This eliminates 3 uses of Obj from TCB.
2018-06-17Remove the proj_body field from the kernel.Pierre-Marie Pédrot
This was completely wrong, such a term could not even be type-checked by the kernel as it was internally using a match construct over a negative record. They were luckily only used in upper layers, namley printing and extraction. Recomputing the projection body might be costly in detyping, but this only happens when the compatibility flag is turned on, which is not the default. Such flag is probably bound to disappear anyways. Extraction should be fixed though so as to define directly primitive projections, similarly to what has been done in native compute.
2018-06-17Remove the proj_eta field of the kernel.Pierre-Marie Pédrot
This field was not used inside the kernel and not used in performance-critical code where caching is essential, so we extrude the code that computes it out of the kernel.
2018-06-17Remove special declaration of primitive projections in the kernel.Pierre-Marie Pédrot
This reduces kernel bloat and removes code from the TCB, as compatibility projections are now retypechecked as normal definitions would have been. This should have no effect on efficiency as this only happens once at definition time.
2018-06-17Getting rid of the const_proj field in the kernel.Pierre-Marie Pédrot
This field used to signal that a constant was the compatibility eta-expansion of a primitive projections, but since a previous cleanup in the kernel it had become useless.
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-26 04:37:44 +0000