aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
Commit message (Collapse)AuthorAge
...
| * | | Fix bug #5096: [vm_compute] is exponentially slower than [native_compute].Gravatar Pierre-Marie Pédrot2016-09-23
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The fix is essentially a revert of f22ad60 that introduced the use of the pretyper version of whd_all instead of the one from the kernel. The exact cause of slowness of the pretyper version is still to be investigated, but it is believed that it is due to a call-by-name strategy, to compare with call-by-need in the kernel. Note that there is still something fishy in presence of evars. Technically vm_compute does not handle them, but if this comes to be the case, it might be worthwile to use an evar-aware variant of whd_all.
* | | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-09-23
|\| | |
| * | | Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-09-23
| |\ \ \ | | | |/ | | |/|
| | * | Fixing #5095 (non relevant too strict test in let-in abstraction).Gravatar Hugo Herbelin2016-09-22
| | | |
* | | | Make the Coq codebase independent from Ltac-related code.Gravatar Pierre-Marie Pédrot2016-09-16
|\ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We untangle many dependencies on Ltac datastructures and modules from the lower strata, resulting in a self-contained ltac/ folder. While not a plugin yet, the change is now very easy to perform. The main API changes have been documented in the dev/doc/changes file. The patches are quite rough, and it may be the case that some parts of the code can migrate back from ltac/ to a core folder. This should be decided on a case-by-case basis, according to a more long-term consideration of what is exactly Ltac-dependent and whatnot.
| * | | | Untangling Tacexpr from lower strata.Gravatar Pierre-Marie Pédrot2016-09-15
| | | | |
* | | | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-09-14
|\ \ \ \ \ | | |/ / / | |/| | |
| * | | | Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-09-14
| |\ \ \ \ | | | |/ / | | |/| |
| * | | | Merge remote-tracking branch 'github-coq/pr/249' into v8.6Gravatar Matthieu Sozeau2016-09-12
| |\ \ \ \
| | | * | | Fixing #5077 (failure on typing a fixpoint with evars in its type).Gravatar Hugo Herbelin2016-09-10
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Typing.type_of was using conversion for types of fixpoints while it could have used unification.
| | * | | | no-refold patchGravatar Paul Steckler2016-09-09
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Add a boolean for refolding during reduction, and an option that is off by default in 8.6, to turn refolding on in all reduction functions, as in 8.5.
| * | | | | Fast path in Clenvtac.clenv_refine typeclass resolution.Gravatar Pierre-Marie Pédrot2016-09-09
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This legacy function is still used by destruct, and is a hotspot in various examples from the wild. We hijack the check from Typeclass and perform a double check at once not to mark unresolvable evars in vain a lot.
* | | | | | Propagate location info on pattern match compilation.Gravatar Emilio Jesus Gallego Arias2016-09-09
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This is a follow-up to #244 and corrects a minor bug introduced by the patch.
| * | | | | Monomorphize a costly boolean equality operation.Gravatar Pierre-Marie Pédrot2016-09-09
| |/ / / /
| | | | * Tracking careless uses of slow name lookup.Gravatar Pierre-Marie Pédrot2016-09-09
| | |_|/ | |/| |
| | | * Unplugging Tacexpr in several interface files.Gravatar Pierre-Marie Pédrot2016-09-08
| |_|/ |/| |
* | | Merge PR #244.Gravatar Pierre-Marie Pédrot2016-09-08
|\ \ \
* | | | CLEANUP: switching from "right-to-left" to "left-to-right" function ↵Gravatar Matej Kosik2016-08-30
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | composition operator. Short story: This pull-request: (1) removes the definition of the "right-to-left" function composition operator (2) adds the definition of the "left-to-right" function composition operator (3) rewrites the code relying on "right-to-left" function composition to rely on "left-to-right" function composition operator instead. Long story: In mathematics, function composition is traditionally denoted with ∘ operator. Ocaml standard library does not provide analogous operator under any name. Batteries Included provides provides two alternatives: _ % _ and _ %> _ The first operator one corresponds to the classical ∘ operator routinely used in mathematics. I.e.: (f4 % f3 % f2 % f1) x ≜ (f4 ∘ f3 ∘ f2 ∘ f1) x We can call it "right-to-left" composition because: - the function we write as first (f4) will be called as last - and the function write as last (f1) will be called as first. The meaning of the second operator is this: (f1 %> f2 %> f3 %> f4) x ≜ (f4 ∘ f3 ∘ f2 ∘ f1) x We can call it "left-to-right" composition because: - the function we write as first (f1) will be called first - and the function we write as last (f4) will be called last That is, the functions are written in the same order in which we write and read them. I think that it makes sense to prefer the "left-to-right" variant because it enables us to write functions in the same order in which they will be actually called and it thus better fits our culture (we read/write from left to right).
* | | | CLEANUP: using |> operator more consistentlyGravatar Matej Kosik2016-08-30
| | | |
* | | | CLEANUP: taking advantage of "_ % _" operator to express function ↵Gravatar Matej Kosik2016-08-29
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | composition in a more obvious way This commit rewrites terms (fun x -> f1 (f2 ... (fN x)...)) to f1 % f2 % ... % fN
* | | | CLEANUP: rename "Context.Named.{to,of}_rel" functions to ↵Gravatar Matej Kosik2016-08-26
| | | | | | | | | | | | | | | | "Context.Named.{to,of}_rel_decl"
* | | | Merge remote-tracking branch 'v8.6' into trunkGravatar Matej Kosik2016-08-25
|\ \ \ \ | | |/ / | |/| |
* | | | CLEANUP: minor readability improvementsGravatar Matej Kosik2016-08-24
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | mainly concerning referring to "Context.{Rel,Named}.get_{id,value,type}" functions. If multiple modules define a function with a same name, e.g.: Context.{Rel,Named}.get_type those calls were prefixed with a corresponding prefix to make sure that it is obvious which function is being called.
* | | | CLEANUP: removing calls of the "Context.Named.Declaration.to_tuple" functionGravatar Matej Kosik2016-08-24
| | | |
* | | | CLEANUP: removing superfluous (module) qualifiersGravatar Matej Kosik2016-08-24
| | | |
* | | | Changing the definition of the "Lib.variable.info" type to enable us to do ↵Gravatar Matej Kosik2016-08-24
| | | | | | | | | | | | | | | | more cleanups
| * | | Merge PR #258: "Fix newline issues" into v8.6Gravatar Pierre-Marie Pédrot2016-08-24
| |\ \ \
| * | | | Pushing error backtrace in unification reraise.Gravatar Pierre-Marie Pédrot2016-08-22
| | | | |
| * | | | Do not recompute the whole evar naming environment in GProd intepretation.Gravatar Pierre-Marie Pédrot2016-08-21
| | | | |
| * | | | Short path for Pretyping.ltac_interp_name_env.Gravatar Pierre-Marie Pédrot2016-08-21
|/ / / / | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Instead of recomputing the evar name environment from scratch when it is unchanged, we simply return the original one. This should fix #4964 for good, although I still find the global evar naming mechanism from Pretyping more than messy. Introducing the heuristic allowing to capture variables from Ltac in constr binders is indeed the root of many evils... That is far from being a zero-cost abstraction!
* | | | Fixing a bug in the presence of let-in while inferring the return clause.Gravatar Hugo Herbelin2016-08-20
| | | |
| | * | Make the user_err header an optional parameter.Gravatar Emilio Jesus Gallego Arias2016-08-19
| | | | | | | | | | | | | | | | Suggested by @ppedrot
| | * | Remove errorlabstrm in favor of user_errGravatar Emilio Jesus Gallego Arias2016-08-19
| | | | | | | | | | | | | | | | | | | | | | | | | | | | As noted by @ppedrot, the first is redundant. The patch is basically a renaming. We didn't make the component optional yet, but this could happen in a future patch.
| | * | Unify location handling of error functions.Gravatar Emilio Jesus Gallego Arias2016-08-19
| |/ / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | In some cases prior to this patch, there were two cases for the same error function, one taking a location, the other not. We unify them by using an option parameter, in the line with recent changes in warnings and feedback. This implies a bit of clean up in some places, but more importantly, is the preparation for subsequent patches making `Loc.location` opaque, change that could be use to improve modularity and allow a more functional implementation strategy --- for example --- of the beautifier.
| * | [pp] Fix newline issues.Gravatar Emilio Jesus Gallego Arias2016-08-19
|/ / | | | | | | | | | | | | | | | | This is a followup to 91ee24b4a7843793a84950379277d92992ba1651 , where we got a few cases wrong wrt to newline endings. Thanks to @herbelin for pointing it out. This doesn't yet fix https://coq.inria.fr/bugs/show_bug.cgi?id=4842
* | Two protections against failures when printing evar_map.Gravatar Hugo Herbelin2016-08-17
| | | | | | | | | | | | | | | | Delimit the scope of the failure to ease potential need for debugging the debugging printer. Protect against one of the causes of failure (calling get_family_sort_of with non-synchronized sigma).
* | Efficiently generate the pretyping contexts.Gravatar Pierre-Marie Pédrot2016-08-16
|\ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | We used to recompute all fresh named contexts for evars before this patch in the push_rel_context_to_named_context function. This was incurring a linear penalty and a memory explosion due to the reallocation of many arrays. Now, we rather remember the context between evar creations by sharing it in the pretyping environment. This can be considered as a fix for bug #4964 even though we might do better.
* | | Make it a bit more obvious when variables are of type unit.Gravatar Guillaume Melquiond2016-08-10
| | |
| * | Using a dedicated kind of substitutions in evar name generation.Gravatar Pierre-Marie Pédrot2016-08-06
| | | | | | | | | | | | This saves a quadratic allocation by replacing arrays with maps.
| * | Using the extended contexts in pretyping.Gravatar Pierre-Marie Pédrot2016-08-05
| | | | | | | | | | | | | | | In addition to sharing, we also delay the computation of the environment in a by-need fashion.
| * | Embedding the pretyping environment in a dummy record.Gravatar Pierre-Marie Pédrot2016-08-04
|/ /
* | A new step on using alpha-conversion in printing notations.Gravatar Hugo Herbelin2016-07-18
| | | | | | | | | | | | | | A couple of bugs have been found. Example #4932 is now printing correctly in the presence of multiple binders (when no let-in, no irrefutable patterns).
* | Partial fix to #4592 (notation requiring alpha-conversion for printing).Gravatar Hugo Herbelin2016-07-17
| |
* | Remove spurious warnings about projections when requiring modules.Gravatar Pierre-Marie Pédrot2016-07-08
| |
* | Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-07-07
|\|
* | Merge remote-tracking branch 'github/bug4653' into v8.6Gravatar Matthieu Sozeau2016-07-07
|\ \
* | | Fix reopened bug #3317.Gravatar Matthieu Sozeau2016-07-06
| | |
* | | Disallow dependent case on prim records w/o etaGravatar Matthieu Sozeau2016-07-06
| | |
* | | Renaming to more generic has_dependent_elim testGravatar Matthieu Sozeau2016-07-06
| | |
* | | Move is_prim... to Inductiveops and correct SchemeGravatar Matthieu Sozeau2016-07-06
| | | | | | | | | | | | | | | | | | | | | | | | Now scheme will not try to build ill-typed dependent analyses on recursive records with primitive projections but report a proper error. Minor change of the API (adding one error case to recursion_scheme_error).
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-07 15:25:53 +0000