2120883307
@Kha I had some unexpected surprises, but it is a good change.
Here is the summary.
1- We could get rid of `a %ₙ b` and `ModN` class. We can use `HMod`
instead. It was a positive surprise since I didn't remember we had
this `ModN` class.
2- Coercions are never used in heterogeneous operators. This is
expected since `a * b` is now notation for `HMul.hMul a b`, and
`a` and `b` may have different types. I manually added instances such
as `HMul Nat Int Int`. However, I did not try to add generic instances
such as
```
instance [Coe a b] [Mul b] : HMul a b b where
hMul x y := mul (coe x) y
```
I will try later.
3- Give `h : cs.size > 0`, I got a type error at
```
let idx : Fin cs.size := ⟨cs.size - 1, Nat.predLt h⟩
```
`Nat.predLt h` has type `Nat.pred cs.size < cs.size`
However, `Nat.pred cs.size` doesn't unify with `cs.size - 1`.
The problem is that we can't synthesize the `HSub` instance until
we apply the default instances.
It worked before because `isDefEq` would force the pending TC
problem `Sub Nat` to be resolved, and after that we would be able
to reduce `cs.size - 1` and establish that it is definitionally
equal to `Nat.pred cs.size`.
I considered two possible workarounds
a) `let idx : Fin cs.size := ⟨cs.size - (1:Nat), Nat.predLt h⟩`
b) `let idx : Fin cs.size := ⟨cs.size - 1, by exact Nat.predLt h⟩`
The first one works because we are not providing enough information
for synthesizing the `HSub` instance. The second works because it
postpones the elaboration of `Nat.predLt h`. The default instances
will be applied before we start applying tactics.
4- The `.` notation is affected too. For example, `(x + 1).toUInt8`
doesn't work since we don't know the type of `x+1` until we apply
default instances. I fixed it by using `(x + (1:Nat)).toUInt8`.
Another possible fix is `Nat.toUInt8 (x + 1)`.
Similarly, `(x+1).fold ...` doesn't work.
5- The following code failed to be elaborated
```
indent (push s!"{ss'}\n") (some (0 - Format.getIndent (← getOptions)))
```
It was working before, but it relied on how the expected type is
propagated. The elaborator process
```
some (0 - Format.getIndent (← getOptions))
```
with expected type `(Option Int)`. So, the `-` is interpreted as
`Int.sub` although `Format.getIndent (← getOptions)` has type `Nat`.
In the new `HSub`, the expected type doesn't really influence TC
resolution since it is an `outparam`. So, we failed with the error
failed to synthesize `HSub Nat Nat Int`.
One possible fix was to add the instance `HSub Nat Nat Int` with
`Int.sub`, but I used the following fix
```
some ((0 : Int) - Format.getIndent (← getOptions))
```
which makes it clear that we want the `Int.sub` operator instead of
`Nat.sub`.
67 lines
2.4 KiB
Text
67 lines
2.4 KiB
Text
#lang lean4
|
||
abbrev Elem := UInt32
|
||
|
||
def badRand (seed : Elem) : Elem :=
|
||
seed * 1664525 + 1013904223
|
||
|
||
def mkRandomArray : Nat → Elem → Array Elem → Array Elem
|
||
| 0, seed, as => as
|
||
| i+1, seed, as => mkRandomArray i (badRand seed) (as.push seed)
|
||
|
||
partial def checkSortedAux (a : Array Elem) : Nat → IO Unit
|
||
| i =>
|
||
if i < a.size - 1 then do
|
||
unless (a.get! i <= a.get! (i+1)) do throw (IO.userError "array is not sorted");
|
||
checkSortedAux a (i+1)
|
||
else
|
||
pure ()
|
||
|
||
-- copied from stdlib, but with `UInt32` indices instead of `Nat` (which is more comparable to the other versions)
|
||
abbrev Idx := UInt32
|
||
|
||
macro:max "↑" x:term:max : term => `(UInt32.toNat $x)
|
||
|
||
@[specialize] private partial def partitionAux {α : Type} [Inhabited α] (lt : α → α → Bool) (hi : Idx) (pivot : α) : Array α → Idx → Idx → Idx × Array α
|
||
| as, i, j =>
|
||
if j < hi then
|
||
if lt (as.get! ↑j) pivot then
|
||
let as := as.swap! ↑i ↑j;
|
||
partitionAux lt hi pivot as (i+1) (j+1)
|
||
else
|
||
partitionAux lt hi pivot as i (j+1)
|
||
else
|
||
let as := as.swap! ↑i ↑hi;
|
||
(i, as)
|
||
|
||
set_option pp.all true
|
||
@[inline] def partition {α : Type} [Inhabited α] (as : Array α) (lt : α → α → Bool) (lo hi : Idx) : Idx × Array α :=
|
||
let mid : Idx := (lo + hi) / 2;
|
||
let as := if lt (as.get! ↑mid) (as.get! ↑lo) then as.swap! ↑lo ↑mid else as;
|
||
let as := if lt (as.get! ↑hi) (as.get! ↑lo) then as.swap! ↑lo ↑hi else as;
|
||
let as := if lt (as.get! ↑mid) (as.get! ↑hi) then as.swap! ↑mid ↑hi else as;
|
||
let pivot := as.get! ↑hi;
|
||
partitionAux lt hi pivot as lo lo
|
||
|
||
@[specialize] partial def qsortAux {α : Type} [Inhabited α] (lt : α → α → Bool) : Array α → Idx → Idx → Array α
|
||
| as, low, high =>
|
||
if low < high then
|
||
let p := partition as lt low high;
|
||
-- TODO: fix `partial` support in the equation compiler, it breaks if we use `let (mid, as) := partition as lt low high`
|
||
let mid := p.1;
|
||
let as := p.2;
|
||
let as := qsortAux lt as low mid;
|
||
qsortAux lt as (mid+1) high
|
||
else as
|
||
|
||
@[inline] def qsort {α : Type} [Inhabited α] (as : Array α) (lt : α → α → Bool) : Array α :=
|
||
qsortAux lt as 0 (UInt32.ofNat (as.size - 1))
|
||
|
||
def main (xs : List String) : IO Unit :=
|
||
do
|
||
let n := xs.head!.toNat!;
|
||
n.forM $ fun _ =>
|
||
n.forM $ fun i => do
|
||
let xs := mkRandomArray i (UInt32.ofNat i) Array.empty;
|
||
let xs := qsort xs (fun a b => a < b);
|
||
--IO.println xs;
|
||
checkSortedAux xs 0
|