Use computed fields for Expr, Level, and Name

[gebner]

Most of the changes are fairly mechanical:

• Remove the underscores.
• Replace | .forallE n d b c => c.binderInfo by | .forallE n d b c => c
• stage0 updates

(I have added the BinderInfo argument at the end, so that the pattern .forallE _ _ b _ doesn't quietly change its meaning.)

All other non-mechanical changes:

• The first commit adds some extra material on the LawfulBEq class, which was useful to define the DecidableEq Name and LawfulBEq Name instances (Init/Core.lean, Init/Meta.lean, Init/Data/List/Basic.lean, Init/Data/Nat/Linear.lean, Init/Prod.lean). The Init/Meta.lean file contains the lawful instances.
• Name patterns no longer need to be special cases (PatternVar.lean)
• Init/Prelude.lean contains the Name refactoring: hash is moved to a computed field, and the smart constructors are made abbreviations (because the RPC encoding deriver otherwise fails to synthesize an instance).
• Lean/Expr.lean contains the Expr refactoring: data is moved to a computed field
• Lean/Level.lean contains the Level refactoring: data is moved to a computed field
• kernel/level.h: adapted, Level.zero is now a scalar
• ReduceEval.lean is adapted to the new name constructor arity.
• AC/Main.lean simplies a @[pattern] definition
• SizeOf.lean: removed an argument from a simp lemma (after this PR, we can probably auto-derive the sizeof instance for names)
• lake is updated to chore: hash field in Name was dropped lake#96

If there was a way to hide the underscore removals from the diff, it would be really short.

[Kha]

!bench

[leanprover-bot]

Here are the benchmark results for commit d105270.
The entire run failed.
Found no significant differences.

[Kha]

Something is rotten in the state of Benchmark...

[Kha]

!bench

[leanprover-bot]

Here are the benchmark results for commit d105270.
The entire run failed.
Found no significant differences.

[leanprover-bot]

Here are the benchmark results for commit d105270.
There were significant changes against commit dd924e5:

  Benchmark                  Metric             Change
  ===============================================================
- libleanshared.so           binary size            2%
- stdlib                     instructions          13% (3367.6 σ)
- stdlib                     linting                7%  (156.4 σ)
- stdlib                     maxrss                 5%  (274.2 σ)
- stdlib                     task-clock            13%  (308.1 σ)
- stdlib                     wall-clock            13%  (388.5 σ)
- stdlib size                bytes .olean           6%
- stdlib size                lines C                4%
- tests/bench/ interpreted   maxrss                 2%   (21.9 σ)
- tests/compiler             sum binary sizes       2%
+ unionfind                  instructions          -1% (-136.3 σ)

[gebner]

Now the diff is a net reduction of 26kLOC. 😄 @Kha Could you please start a new benchmark run?

[Kha]

!bench

[leanprover-bot]

Here are the benchmark results for commit 78731e6.
There were significant changes against commit 75b0b50:

  Benchmark     Metric         Change
  ===============================================
- stdlib        instructions       8% (17640.5 σ)
- stdlib        linting            5%   (306.3 σ)
- stdlib        maxrss             4%   (231.1 σ)
- stdlib        task-clock         8%   (323.6 σ)
- stdlib        wall-clock         9%    (14.5 σ)
- stdlib size   bytes .olean       4%
- unionfind     task-clock         4%    (12.1 σ)
- unionfind     wall-clock         4%    (11.9 σ)

[gebner]

Okay, added back the extern c inline "lean_ctor_get_uint64(#1, lean_ctor_num_objs(#1)*sizeof(void*))". Maybe that helps.

@Kha Could you please start a new benchmark run?

[Kha]

!bench

[gebner]

Oops, forgot the borrow annotation. :-/ @Kha Can I bother you again?

[Kha]

Actually you might have sufficient permissions to trigger it yourself?

[leanprover-bot]

Here are the benchmark results for commit 36e5353.
There were significant changes against commit 75b0b50:

  Benchmark                  Metric             Change
  =================================================================
- stdlib                     instructions          11%   (3818.1 σ)
- stdlib                     linting                5%    (232.5 σ)
- stdlib                     maxrss               141%   (4736.4 σ)
- stdlib                     task-clock            10% (642493.9 σ)
- stdlib                     wall-clock            11%     (49.1 σ)
- stdlib size                bytes .olean           4%
- tests/bench/ interpreted   maxrss                26%     (84.0 σ)
- tests/compiler             sum binary sizes       2%

[gebner]

!bench

[leanprover-bot]

Here are the benchmark results for commit 9937d42.
There were significant changes against commit 75b0b50:

  Benchmark                  Metric             Change
  ===============================================================
- stdlib                     instructions           7% (6501.0 σ)
- stdlib                     linting                5%  (153.7 σ)
- stdlib                     maxrss                 4%   (60.1 σ)
- stdlib                     task-clock             7%  (368.8 σ)
- stdlib                     wall-clock             8%   (26.4 σ)
- stdlib size                bytes .olean           4%
- tests/bench/ interpreted   maxrss                 1%   (10.3 σ)
- tests/compiler             sum binary sizes       2%
- unionfind                  task-clock             4%   (14.9 σ)
- unionfind                  wall-clock             4%   (14.6 σ)

[gebner]

!bench

[leanprover-bot]

Here are the benchmark results for commit ad1d244.
There were significant changes against commit a6151a9:

  Benchmark                  Metric             Change
  ===============================================================
+ binarytrees                task-clock            -3%  (-16.9 σ)
- stdlib                     instructions           7% (6389.4 σ)
- stdlib                     linting                5%   (71.3 σ)
- stdlib                     maxrss                 4%  (535.2 σ)
- stdlib                     task-clock             7%  (105.0 σ)
- stdlib                     wall-clock             7%   (19.8 σ)
- stdlib size                bytes .olean           4%
- tests/bench/ interpreted   maxrss                 1%   (27.0 σ)
- tests/compiler             sum binary sizes       2%

[gebner]

!bench

[leanprover-bot]

Here are the benchmark results for commit 03a6a35.
There were significant changes against commit 23bae26:

  Benchmark                  Metric             Change
  ===============================================================
- stdlib                     instructions           5% (2352.0 σ)
- stdlib                     linting                7%   (15.6 σ)
- stdlib                     maxrss                 4%  (729.6 σ)
- stdlib                     task-clock             5%  (231.5 σ)
- stdlib                     wall-clock             6%   (81.6 σ)
- stdlib size                bytes .olean           4%
- tests/bench/ interpreted   maxrss                 1%   (11.6 σ)
- tests/compiler             sum binary sizes       2%

[gebner]

!bench

[leanprover-bot]

Here are the benchmark results for commit 55d2c08.
There were significant changes against commit 23bae26:

  Benchmark        Metric             Change
  =====================================================
- stdlib           instructions           5% (1993.3 σ)
- stdlib           linting                7%   (14.1 σ)
- stdlib           maxrss                 4%  (264.5 σ)
- stdlib           task-clock             5%  (113.3 σ)
- stdlib           wall-clock             5%  (141.0 σ)
- stdlib size      bytes .olean           4%
- tests/compiler   sum binary sizes       2%

[gebner]

I'm still at a loss where the 5% stdlib runtime increase comes from, but I've found an exciting related bug. It turns out that Expr.updateApp! and co. have been broken for some time, and always constructed a new expression. As a result, the following printed false:

import Lean
open Lean

#eval
  let e := mkApp (mkSort levelZero) (mkSort levelZero)
  let e' := e.replace fun _ => none
  ptrAddrUnsafe e == ptrAddrUnsafe e'

The reason is a missed optimization:

set_option trace.compiler.ir.result true

inductive Exp
  | var (i : Nat)
  | app (a b : Exp)

def Exp.hash : Exp → Nat
    | .var i => i
    | .app a b => a.hash + b.hash

def Exp.complicatedHash : Exp → Nat
  | app a b =>
    -- This always constructs an `app a b`-object, even though we could reuse the input.
    (app a b).hash
  | e => e.hash

I've reimplemented all the update* functions in Lean and they now behave as they should.

[gebner]

!bench

[leanprover-bot]

Here are the benchmark results for commit 02362f4.
There were significant changes against commit 2fcd406:

  Benchmark        Metric             Change
  =====================================================
- stdlib           instructions           5% (3240.5 σ)
- stdlib           linting               14%  (139.8 σ)
- stdlib           maxrss                 4%   (35.0 σ)
- stdlib           task-clock             5%  (287.9 σ)
- stdlib           wall-clock             6%  (229.3 σ)
- stdlib size      bytes .olean           4%
- tests/compiler   sum binary sizes       2%

[gebner]

!bench

[leanprover-bot]

Here are the benchmark results for commit 12be539.
There were significant changes against commit 2fcd406:

  Benchmark        Metric             Change
  ===================================================
- stdlib           linting                8% (59.1 σ)
- stdlib           maxrss                 4% (67.8 σ)
- stdlib size      bytes .olean           4%
- tests/compiler   sum binary sizes       2%

[gebner]

I've added a list of changes in the PR description.

[leodemoura]

It is not clear to me why we need this change.
I will investigate after we merge.

[leodemoura]

Same here.

[gebner]

Those are from the first commit, which added the beq_iff_eq simp lemma. The previous proof used a "nonterminal simp", which are very likely to break when changing the library.

[leodemoura]

I am assuming --" is some kind of "leftover".

[leodemoura]

Unnecessary ..

[leodemoura]

I have only minor issues. We can address them after the merge. I just enabled the auto-merge.