aboutsummaryrefslogtreecommitdiff
path: root/pretyping
AgeCommit message (Collapse)Author
2020-09-28More precise information when unification fails because of incompatible ↵Hugo Herbelin
candidates. We also show the incompatible contender. Ideally, we should also remember the source of the other contender.
2020-09-03Comment AllowedEvars APIMaxime Dénès
2020-09-02More efficient data structure for allowed evarsMaxime Dénès
2020-09-02Abstract type for allowed evarsMaxime Dénès
2020-09-02Replace `frozen` by `allowed` evars in evarconv, and delay themMaxime Dénès
This is a follow-up of #9062, which introduced a discrenpancy between the two unification engines.
2020-08-31Use a faster algorithm to check for class existence.Pierre-Marie Pédrot
There is a hidden invariant that guarantees that the class index and its reference field are the same.
2020-08-27Merge PR #12849: Rename VM-related kernel/cfoo files to kernel/vmfooPierre-Marie Pédrot
Reviewed-by: gares Reviewed-by: ppedrot Reviewed-by: silene
2020-08-19Merge PR #12725: Store evar identity instances in evarinfo / named_context_valEnrico Tassi
Ack-by: SkySkimmer Reviewed-by: gares
2020-08-18Rename VM-related kernel/cfoo files to kernel/vmfooGaëtan Gilbert
2020-08-17Merge PR #12751: Fixes reduction effect printing in the presence of non ↵Pierre-Marie Pédrot
purely applicative stacks Ack-by: SkySkimmer Reviewed-by: ppedrot
2020-08-11Small code simplification in contract_(co)fix.Pierre-Marie Pédrot
Probably a remnant of a time where the difference in code path was relevant.
2020-08-11Move reduce_mind_case from Reductionops to Tacred.Pierre-Marie Pédrot
It was only used there, and its API required to export an ad-hoc type to represent pattern-matchings.
2020-08-06Actually use the default instance stored inside named_context_val.Pierre-Marie Pédrot
2020-08-06Use the evarinfo-stored identity substitution where applicable.Pierre-Marie Pédrot
2020-07-24Fixes reduction effect printing in the presence of non purely applicative ↵Hugo Herbelin
stacks.
2020-07-22Remove redundant data from VM case switch.Pierre-Marie Pédrot
No need to store the case_info, all the data is reconstructible from the context. Furthermore, this reconstruction is performed in a context where we already access the environment, so performance is not at stake. Hopefully this will also reduce the number of globally allocated VM values, since the switch representation now only depends on the shape of the inductive type.
2020-07-18Merge PR #12588: [exn] Remove some uses of printPierre-Marie Pédrot
Ack-by: gares Reviewed-by: ppedrot
2020-07-13Don't catch anomalies for evarconv "cannot find an instance" errorGaëtan Gilbert
2020-07-11Merge PR #12650: Recordops: unify struc_typ summary record and libobject ↵Pierre-Marie Pédrot
entry struc_tuple Reviewed-by: ppedrot
2020-07-11Merge PR #12646: Correctly readback blocked CaseInvert matches in VM/nativePierre-Marie Pédrot
Reviewed-by: ppedrot
2020-07-10Merge PR #12638: Some changes of representation in TacredEnrico Tassi
Ack-by: backtracking Reviewed-by: gares
2020-07-09[error handling] Anomaly in Conversion is a "precatchable_exception"Emilio Jesus Gallego Arias
This is just a fixup, likely all the places that are matching on `UserErr` directly are just buggy.
2020-07-09[reductionops] Comment about absorption of anomalies.Emilio Jesus Gallego Arias
Co-authored-by: <Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
2020-07-09[exn] Remove some uses of printEmilio Jesus Gallego Arias
Exceptions should not printed except for the top-level. There is the weird anomaly-absorbing code in `Reductionops`, I wonder how frequent that case is, but as the exception is absorbed printing there could have a real impact.
2020-07-09Recordops: unify struc_typ summary record and libobject entry struc_tupleGaëtan Gilbert
This requires updating the parameter count at section end, I felt it was easier to do with rebuild_function but it could be done in discharge if needed. Incidentally fixes #12649.
2020-07-08Merge PR #12627: Fix Canonical with universe polymorphism and primitive ↵Enrico Tassi
projection Reviewed-by: ejgallego Ack-by: gares
2020-07-08Remove Evarutil.new_evar_instance from the API.Pierre-Marie Pédrot
2020-07-06Correctly readback blocked CaseInvert matches in VM/nativeGaëtan Gilbert
2020-07-06Primitive persistent arraysMaxime Dénès
Persistent arrays expose a functional interface but are implemented using an imperative data structure. The OCaml implementation is based on Jean-Christophe Filliâtre's. Co-authored-by: Benjamin Grégoire <Benjamin.Gregoire@inria.fr> Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
2020-07-05Further cleanup of dead code in the Reductionops API.Pierre-Marie Pédrot
2020-07-05Remove the last use of the Stack module in Tacred.Pierre-Marie Pédrot
2020-07-05Inline make_elim_fun in Tacred.Pierre-Marie Pédrot
We seize the opportunity to simplify the code and hoist out computations that can be avoided.
2020-07-05Inline the Reductionops.fix_recarg function.Pierre-Marie Pédrot
It was only used in Tacred, and with a type that forced to perform a change of representation of stacks.
2020-07-05Inline mutual recursion helpers in simpl implementation.Pierre-Marie Pédrot
This highlights static invariants about the function.
2020-07-05Stop back-and-forth array to list conversions in simpl.Pierre-Marie Pédrot
2020-07-05Fix Canonical with universe polymorphism and primitive projectionGaëtan Gilbert
Perhaps we should thread an evar map with the Var universes added through to cs_pattern_of_constr but that would be significantly more invasive. Fix #12528
2020-07-01UIP in SPropGaëtan Gilbert
2020-06-23Merge PR #12530: Fix glob_sort_family for SPropMaxime Dénès
Reviewed-by: gares Reviewed-by: maximedenes
2020-06-19Share the identity instance in pretyping environments.Pierre-Marie Pédrot
2020-06-19Do not reallocate named_context_val of the pretyping environment.Pierre-Marie Pédrot
Instead of costly linear reallocations, we share as much as possible of the prefixes of the various environment subcomponents.
2020-06-17Fix glob_sort_family for SPropGaëtan Gilbert
Fixes #12529
2020-06-04Move the Cbn module to tactics/.Pierre-Marie Pédrot
2020-06-04Further cleanup.Pierre-Marie Pédrot
We factorize code between Cbn and Reductionops, and remove dead code as well.
2020-06-04Move the cbn reduction to its own file, and simplify the RAKAM accordingly.Pierre-Marie Pédrot
2020-05-29Fixes #12418 (inference of return clause meets assert false).Hugo Herbelin
This is a quick fix to avoid the anomaly, with a fallback on before b1b8243b7fc.
2020-05-22Merge PR #12295: Fixes #12233: printing environment corrupted with ↵Pierre-Marie Pédrot
eta-expansion of "match" branches Reviewed-by: gares Ack-by: ppedrot
2020-05-15[misc] Better preserve backtraces in several modulesEmilio Jesus Gallego Arias
Re-raising inside exception handlers must be done with care in order to preserve backtraces; even if newer OCaml versions do a better job in automatically spilling `%reraise` in places that matter, there is no guarantee for that to happen. I've done a best-effort pass of places that were re-raising incorrectly, hopefully I got the logic right. There is the special case of `Nametab.error_global_not_found` which is raised many times in response to a `Not_found` error; IMHO this error should be converted to something more specific, however the scope of that change would be huge as to do easily...
2020-05-14Merge PR #11922: No more local reduction functions in Reductionops.Maxime Dénès
Reviewed-by: Matafou Ack-by: SkySkimmer Reviewed-by: gares
2020-05-13Fixes #12233 (wrong printing env in presence of match branches eta-expansion).Hugo Herbelin
At the same time, we propagate the correct binder relevance in detyping. Note that this would be fixed by enforcing the context of branches in the syntax of "Case".
2020-05-12Do not use Unsafe.to_constr for old refiner conclusion.Pierre-Marie Pédrot
This was useless, since we did not observe the difference on evars.
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-09 16:22:18 +0000