aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel
Commit message (Collapse)AuthorAge
* Term_typing: remove unused argument to internal function.Gravatar Gaëtan Gilbert2018-07-03
| | | | | | | 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.
* Cooking.cook_constant: remove unused env argument.Gravatar Gaëtan Gilbert2018-07-03
| | | | Unused since d95306323 (remove template polymorphic definitions).
* Indtypes: remove unused is_unit.Gravatar Gaëtan Gilbert2018-07-03
|
* Subtyping.check_constant: remove unused module path argument.Gravatar Gaëtan Gilbert2018-07-03
|
* Inductive.extract_stack,filter_stack_domain: remove unused argumentsGravatar Gaëtan Gilbert2018-07-03
|
* Nativecode compile_mind, compile_mind_field: remove unused argumentsGravatar Gaëtan Gilbert2018-07-03
|
* Nativecode.pp_mllam internal pp_letrec: remove unused argument.Gravatar Gaëtan Gilbert2018-07-03
|
* Modops.add_retroknowledge: remove unused argument.Gravatar Gaëtan Gilbert2018-07-03
| | | | | | 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.
* Merge PR #7080: Swapping Context and Constr and defining declarations on ↵Gravatar Maxime Dénès2018-06-29
|\ | | | | | | constr in Constr
* | Deprecate Environ.retroknowledge function in favor of the projectionGravatar Gaëtan Gilbert2018-06-28
| |
* | [env.env_rel_context.env_rel_ctx] -> [rel_context env]Gravatar Gaëtan Gilbert2018-06-28
| | | | | | | | It's a bit shorter and more direct.
* | Make Environ.globals abstract.Gravatar Gaëtan Gilbert2018-06-28
| |
* | Merge PR #7768: Fix #7723 (vm_compute segfault and proof of false)Gravatar Pierre-Marie Pédrot2018-06-27
|\ \
| | * Swapping Context and Constr: defining declarations on constr in Constr.Gravatar Hugo Herbelin2018-06-27
| |/ |/| | | | | | | | | | | | | | | 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).
* | Merge PR #7863: Remove Sorts.contentsGravatar Pierre-Marie Pédrot2018-06-27
|\ \
| | * Test file for #7723Gravatar Maxime Dénès2018-06-27
| | |
| | * Fix #7723: vm_compute segfaults with universe polymorphismGravatar Maxime Dénès2018-06-27
| |/ |/| | | | | Was revealing a critical bug in VM universe handling introduced in 8.5.
* | Merge PR #7919: Fix equality check on global names from native compute.Gravatar Maxime Dénès2018-06-26
|\ \
| | * Remove Sorts.contentsGravatar Gaëtan Gilbert2018-06-26
| |/ |/|
* | Merge PR #7798: Remove hack skipping comparison of algebraic universes in ↵Gravatar Matthieu Sozeau2018-06-25
|\ \ | | | | | | | | | subtyping.
| | * Fix equality check on global names from native compute.Gravatar Pierre-Marie Pédrot2018-06-25
| |/ |/| | | | | | | | | 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.
* | Merge PR #7772: [native_compute] Delay computations with toplevel matchGravatar Pierre-Marie Pédrot2018-06-24
|\ \
* \ \ Merge PR #7614: Simplify the code that handles trust of side-effects in ↵Gravatar Maxime Dénès2018-06-23
|\ \ \ | | | | | | | | | | | | kernel typing.
* | | | Adapt the kernel to generate proper data for mutual records.Gravatar Pierre-Marie Pédrot2018-06-23
| | | | | | | | | | | | | | | | Upper layers are still not able to handle mutual records though.
* | | | Using more general information for primitive records.Gravatar Pierre-Marie Pédrot2018-06-23
| | | | | | | | | | | | | | | | | | | | This brings more compatibility with handling of mutual primitive records in the kernel.
* | | | Change the proj_ind field from MutInd.t to inductive.Gravatar Pierre-Marie Pédrot2018-06-23
| | | | | | | | | | | | | | | | | | | | This is a first step towards the acceptance of mutual record types in the kernel.
* | | | Merge PR #7715: Simplify the cooking of primitive projections.Gravatar Maxime Dénès2018-06-23
|\ \ \ \
* \ \ \ \ Merge PR #7600: Faster and cleaner fconstr-to-constr conversion function.Gravatar Maxime Dénès2018-06-22
|\ \ \ \ \
| | | | | * Remove hack skipping comparison of algebraic universes in subtyping.Gravatar Gaëtan Gilbert2018-06-22
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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!).
| | | | | * Define and use UGraph.enforce_leq_alg for subtyping inferenceGravatar Gaëtan Gilbert2018-06-22
| | | | | | | | | | | | | | | | | | | | | | | | Not sure if worth using in other places.
| | | | | * Fix Univ.enforce_leq dropped constraints when algebraic on the rightGravatar Gaëtan Gilbert2018-06-19
| |_|_|_|/ |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | There's probably a proof of false using subtyping if someone wants to look. NB: the checker doesn't handle algebraics on the right.
* | | | | Merge PR #7841: Remove CanaryGravatar Pierre-Marie Pédrot2018-06-19
|\ \ \ \ \
| * | | | | Remove Canary.Gravatar whitequark2018-06-18
| | | | | | | | | | | | | | | | | | | | | | | | This eliminates 3 uses of Obj from TCB.
* | | | | | Remove the proj_body field from the kernel.Gravatar Pierre-Marie Pédrot2018-06-17
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
* | | | | | Remove the proj_eta field of the kernel.Gravatar Pierre-Marie Pédrot2018-06-17
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
* | | | | | Remove special declaration of primitive projections in the kernel.Gravatar Pierre-Marie Pédrot2018-06-17
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
* | | | | | Getting rid of the const_proj field in the kernel.Gravatar Pierre-Marie Pédrot2018-06-17
|/ / / / / | | | | | | | | | | | | | | | | | | | | | | | | | 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.
| * / / / Faster and cleaner fconstr-to-constr conversion function.Gravatar Pierre-Marie Pédrot2018-06-17
|/ / / / | | | | | | | | | | | | | | | | | | | | | | | | | | | | We untangle the implementation in several ways. - No higher-order self argument function as there is only one caller. - Compute composition of lifts + substitution on terms using a dedicated function instead of mk_clos followed by to_constr. - Take more advantage of identity substitutions.
* | | | Merge PR #7635: Define rec_declaration in terms of prec_declaration.Gravatar Maxime Dénès2018-06-17
|\ \ \ \
* \ \ \ \ Merge PR #7616: Fix #7615: Functor inlining drops universe substitution.Gravatar Maxime Dénès2018-06-17
|\ \ \ \ \
* \ \ \ \ \ Merge PR #7677: [api] Remove MisctypesGravatar Pierre-Marie Pédrot2018-06-13
|\ \ \ \ \ \
| * | | | | | [api] Misctypes removal: miscellaneous aliases.Gravatar Emilio Jesus Gallego Arias2018-06-12
| | | | | | |
* | | | | | | [VM] Rename reloc -> cenvGravatar Maxime Dénès2018-06-12
|/ / / / / / | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The renaming is internal only. I believe the name reloc is legacy and a bit confusing now that the structure contains a full compilation environment.
| | | * / / Simplify the cooking of primitive projections.Gravatar Pierre-Marie Pédrot2018-06-11
| |_|/ / / |/| | | | | | | | | | | | | | | | | | | | | | | | There is no need to expand a primitive projection with the section parameters and universes, for one good reason: they are never applied neither to parameters nor universe instances.
| | | | * [native_compute] Delay computations with toplevel matchGravatar Maxime Dénès2018-06-11
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This is an easy improvement on examples like: Fixpoint zero (n : nat) := match n with | O => O | S p => zero p + zero p end. Definition foo := if true then zero 100 else 0. Eval native_compute in if true then 0 else foo. I didn't add a test case, because our current testing infrastructure is too fragile for that.
* | | | | [VM] Remove projection names from structured constants.Gravatar Maxime Dénès2018-06-10
| |_|_|/ |/| | | | | | | | | | | | | | | | | | | | | | | It was actually a hack since those names are never used to represent values, only to be passed as arguments to bytecode instructions. So instead of reusing the structured_constant type, we follow the same pattern as switch annotations.
| * | | Fix #7615: Functor inlining drops universe substitution.Gravatar Pierre-Marie Pédrot2018-06-07
|/ / / | | | | | | | | | | | | | | | | | | We store the universe context in the inlined terms and apply it to the instance provided to the substitution function. Technically the context is not needed, but we use it to assert that the length of the instance corresponds, just in case.
| * | Define rec_declaration in terms of prec_declaration.Gravatar SimonBoulier2018-06-05
| | | | | | | | | | | | And similarly for fixpoint and cofixpoint.
* | | More straightforward native compilation of primitive projections.Gravatar Pierre-Marie Pédrot2018-06-05
| | | | | | | | | | | | | | | | | | Instead of having a constant-based compilation of projections, we generate them at the compilation time of the inductive block to which they pertain.
* | | Use projection indices in native compilation rather than constant names.Gravatar Pierre-Marie Pédrot2018-06-05
|/ /
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-23 18:57:36 +0000