1c20b53419
Implements a new method to generate instance names for anonymous instances that uses a heuristic that tends to produce shorter names. A design goal is to make them relatively unique within projects and definitely unique across projects, while also using accessible names so that they can be referred to as needed, both in Lean code and in discussions. The new method also takes into account binders provided to the instance, and it adds project-based suffixes. Despite this, a median new name is 73% its original auto-generated length. (Compare: [old generated names](https://gist.github.com/kmill/b72bb43f5b01dafef41eb1d2e57a8237) and [new generated names](https://gist.github.com/kmill/393acc82e7a8d67fc7387829f4ed547e).) Some notes: * The naming is sensitive to what is explicitly provided as a binder vs what is provided via a `variable`. It does not make use of `variable`s since, when names are generated, it is not yet known which variables are used in the body of the instance. * If the instance name refers to declarations in the current "project" (given by the root module), then it does not add a suffix. Otherwise, it adds the project name as a suffix to protect against cross-project collisions. * `set_option trace.Elab.instance.mkInstanceName true` can be used to see what name the auto-generator would give, even if the instance already has an explicit name. There were a number of instances that were referred to explicitly in meta code, and these have been given explicit names. Removes the unused `Lean.Elab.mkFreshInstanceName` along with the Command state's `nextInstIdx`. Fixes #2343
107 lines
2.5 KiB
Text
107 lines
2.5 KiB
Text
import Lean
|
||
|
||
open Lean
|
||
|
||
#eval Compiler.compile #[``List.map]
|
||
|
||
#eval Compiler.compile #[``Lean.Elab.Term.synthesizeInstMVarCore]
|
||
|
||
#eval Compiler.compile #[``Eq.ndrec]
|
||
|
||
def g1 (x : Nat) (h : Nat = Int) : Int :=
|
||
(h ▸ x) + 1
|
||
|
||
#eval Compiler.compile #[``g1]
|
||
|
||
def f (h : False) (x : Nat) : Nat :=
|
||
(h.rec : Nat → Nat) x
|
||
|
||
#eval Compiler.compile #[``f]
|
||
|
||
def g (as : Array (Nat → Nat)) (h : i < as.size ∧ q) : Nat :=
|
||
h.casesOn (fun _ _ => as[i]) i
|
||
|
||
#eval Compiler.compile #[``g]
|
||
|
||
def f2 {r : Nat → Nat → Prop} (q : Quot r) : Nat :=
|
||
(q.lift (·+·) sorry : Nat → Nat) 2
|
||
|
||
#eval Compiler.compile #[``f2]
|
||
|
||
inductive Vec (α : Type u) : Nat → Type u
|
||
| nil : Vec α 0
|
||
| cons : α → Vec α n → Vec α (n+1)
|
||
|
||
def Vec.zip : Vec α n → Vec β n → Vec (α × β) n
|
||
| .cons a as, .cons b bs => .cons (a, b) (zip as bs)
|
||
| .nil, .nil => .nil
|
||
|
||
def Vec.head : Vec α (n+1) → α
|
||
| .cons a _ => a
|
||
|
||
#eval Compiler.compile #[``Lean.Elab.Term.reportStuckSyntheticMVar]
|
||
|
||
#eval Compiler.compile #[``Lean.Elab.Term.synthesizeSyntheticMVars]
|
||
|
||
set_option profiler true
|
||
#eval Compiler.compile #[``Lean.Meta.isExprDefEqAuxImpl]
|
||
|
||
def foo (a b : Nat) :=
|
||
let d := match a with
|
||
| .zero => b
|
||
| .succ c => c
|
||
let e := match b with
|
||
| .zero => a
|
||
| .succ f => f
|
||
Nat.add d e
|
||
|
||
#eval Compiler.compile #[``foo]
|
||
|
||
#eval Compiler.compile #[``Vec.zip]
|
||
|
||
|
||
structure Foo where
|
||
α : Sort u
|
||
x : α
|
||
|
||
def foo1 := Foo.mk Type Nat
|
||
|
||
#eval Compiler.compile #[``foo1]
|
||
|
||
def Tuple (α : Type u) : Nat → Type u
|
||
| 0 => PUnit
|
||
| 1 => α
|
||
| n+2 => α × Tuple α (n+1)
|
||
|
||
def mkConstTuple (a : α) : (n : Nat) → Tuple α n
|
||
| 0 => ⟨⟩
|
||
| 1 => a
|
||
| n+2 => (a, mkConstTuple a (n+1))
|
||
|
||
def Tuple.map (f : α → β) (xs : Tuple α n) : Tuple β n :=
|
||
match n with
|
||
| 0 => ⟨⟩
|
||
| 1 => f xs
|
||
| _+2 => match xs with
|
||
| (a, xs) => (f a, Tuple.map f xs)
|
||
|
||
def Tuple.example (a b : Nat) :=
|
||
Tuple.map (n := 2) (· + 1) (a, b)
|
||
|
||
#eval Compiler.compile #[``mkConstTuple]
|
||
#eval Compiler.compile #[``Tuple.map]
|
||
#eval Compiler.compile #[``Tuple.example]
|
||
|
||
def gebner1 (x : UInt64) : UInt64 := assert! x > 0; x - 1
|
||
-- set_option pp.letVarTypes true in
|
||
#eval Compiler.compile #[``gebner1]
|
||
|
||
def gebner2 (x : UInt64) := x &&& ((1 : UInt64) <<< 5 : UInt64)
|
||
-- set_option pp.letVarTypes true in
|
||
#eval Compiler.compile #[``gebner2]
|
||
|
||
#eval Compiler.compile #[``Lean.Meta.instMonadMetaM]
|
||
#eval Compiler.compile #[``Lean.Core.instMonadCoreM]
|
||
#eval Compiler.compile #[``instMonadEIO]
|
||
-- set_option pp.explicit true in
|
||
#eval Compiler.compile #[``EStateM.instMonad]
|