This PR fixes a bug in the projection over constructor propagator used
in `grind`. It may construct type incorrect terms when a equivalence
class contains heterogeneous equalities.
closes#9769
We compute the liveness information for the join point body, so the only
thing that updateJPLiveVarMap should be adding is the binding of the
params, which we can easily do ourselves.
If we supported recursive join points, I believe this would actually be
a correctness issue, but as-is it doesn't affect the output.
This PR fixes the documentation of the pipe operator |>, which is
currently (emphasis mine):
> Haskell-like pipe operator `|>`. `x |> f` means **the same as the same
as** `f x`,
> and it chains such that `x |> f |> g` is interpreted as `g (f x)`.
This PR implements the option `mvcgen +jp` to employ a slightly lossy VC
encoding for join points that prevents exponential VC blowup incurred by
naïve splitting on control flow.
```lean
def ifs_pure (n : Nat) : Id Nat := do
let mut x := 0
if n > 0 then x := x + 1 else x := x + 2
if n > 1 then x := x + 3 else x := x + 4
if n > 2 then x := x + 1 else x := x + 2
if n > 3 then x := x + 1 else x := x + 2
if n > 4 then x := x + 1 else x := x + 2
if n > 5 then x := x + 1 else x := x + 2
return x
theorem ifs_pure_triple : ⦃⌜True⌝⦄ ifs_pure n ⦃⇓ r => ⌜r > 0⌝⦄ := by
unfold ifs_pure
mvcgen +jp
/-
...
h✝⁵ : if n > 0 then x✝⁵ = 0 + 1 else x✝⁵ = 0 + 2
h✝⁴ : if n > 1 then x✝⁴ = x✝⁵ + 3 else x✝⁴ = x✝⁵ + 4
h✝³ : if n > 2 then x✝³ = x✝⁴ + 1 else x✝³ = x✝⁴ + 2
h✝² : if n > 3 then x✝² = x✝³ + 1 else x✝² = x✝³ + 2
h✝¹ : if n > 4 then x✝¹ = x✝² + 1 else x✝¹ = x✝² + 2
h✝ : if n > 5 then x✝ = x✝¹ + 1 else x✝ = x✝¹ + 2
⊢ x✝ > 0
-/
grind
```
This PR does what #9234 regrettably failed to do: actually reintroduce
the signatures of some `Subarray` functions that are now implemented via
slices (see #9017) in order to ensure backward compatibility and
consistency. With this PR, the old interface is restored. As an added
benefit, `Subarray.forIn` is no longer opaque.
This PR re-implements `IO.waitAny` using Lean instead of C++. This is to
reduce the size and
complexity of `task_manager` in order to ease future refactorings.
There is an import behavioral change of `IO.waitAny` in this PR.
Consider a situation where we have
two promises `p1`, `p2` and call `IO.waitAny [p1.result!, p2.result!]`
and `p1` resolves instantly.
Previously this would just return the result of `p1` and require nothing
else. With the new
implementation if `p2` is released before being resolved this can cause
a panic, even if
`IO.waitAny` has already finished. I argue that this is reasonable
behavior, given that an
invocation of `result!` promises that the promise will eventually be
resolved.
This PR moves the validation of cross-package `import all` to Lake and
the syntax validation of import keywords (`public`, `meta`, and `all`)
to the two import parsers.
It also fixes the error reporting of the fast import parser
(`Lean.parseImports`) and adds positions to its errors.
This PR addresses an outstanding feature in the module system to
automatically mark `let rec` and `where` helper declarations as private
unless they are defined in a public context such as under `@[expose]`.
This PR removes an error which implicitly assumes that the sort of type
dependency between erased types present in the test being added can not
occur. It would be difficult to refine the error using only the
information present in LCNF types, and it is of very little ongoing
value (I don't recall it ever finding an actual problem), so it makes
more sense to delete it.
Fixes#9692.
