max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: parameterize DiscrTree indicating whether non trivial reductions are allowed or not when indexing/retrieving terms

Browse source
This commit is contained in:
Leonardo de Moura 2022-11-15 16:27:57 -08:00
parent 81c84bf045
commit 1b0c2f7157
8 changed files with 166 additions and 74 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

94
src/Lean/Meta/DiscrTree.lean
View file

@ -47,7 +47,7 @@ namespace Lean.Meta.DiscrTree
2- Distinguish partial applications `f a`, `f a b`, and `f a b c`.
-/
def Key.ctorIdx : Key → Nat
def Key.ctorIdx : Key s → Nat
| .star => 0
| .other => 1
| .lit .. => 2
@ -56,17 +56,17 @@ def Key.ctorIdx : Key → Nat
| .arrow => 5
| .proj .. => 6
def Key.lt : Key → Key → Bool
def Key.lt : Key s → Key s → Bool
| .lit v₁, .lit v₂ => v₁ < v₂
| .fvar n₁ a₁, .fvar n₂ a₂ => Name.quickLt n₁.name n₂.name || (n₁ == n₂ && a₁ < a₂)
| .const n₁ a₁, .const n₂ a₂ => Name.quickLt n₁ n₂ || (n₁ == n₂ && a₁ < a₂)
| .proj s₁ i₁, .proj s₂ i₂ => Name.quickLt s₁ s₂ || (s₁ == s₂ && i₁ < i₂)
| k₁, k₂ => k₁.ctorIdx < k₂.ctorIdx
instance : LT Key := ⟨fun a b => Key.lt a b⟩
instance (a b : Key) : Decidable (a < b) := inferInstanceAs (Decidable (Key.lt a b))
instance : LT (Key s) := ⟨fun a b => Key.lt a b⟩
instance (a b : Key s) : Decidable (a < b) := inferInstanceAs (Decidable (Key.lt a b))
def Key.format : Key → Format
def Key.format : Key s → Format
| .star => "*"
| .other => "◾"
| .lit (Literal.natVal v) => Std.format v
@ -76,41 +76,41 @@ def Key.format : Key → Format
| .fvar k _ => Std.format k.name
| .arrow => "→"
instance : ToFormat Key := ⟨Key.format⟩
instance : ToFormat (Key s) := ⟨Key.format⟩
def Key.arity : Key → Nat
def Key.arity : (Key s) → Nat
| .const _ a => a
| .fvar _ a => a
| .arrow => 2
| .proj .. => 1
| _ => 0
instance : Inhabited (Trie α) := ⟨.node #[] #[]⟩
instance : Inhabited (Trie α s) := ⟨.node #[] #[]⟩
def empty : DiscrTree α := { root := {} }
def empty : DiscrTree α s := { root := {} }
partial def Trie.format [ToFormat α] : Trie α → Format
partial def Trie.format [ToFormat α] : Trie α s → Format
| .node vs cs => Format.group $ Format.paren $
"node" ++ (if vs.isEmpty then Format.nil else " " ++ Std.format vs)
++ Format.join (cs.toList.map fun ⟨k, c⟩ => Format.line ++ Format.paren (Std.format k ++ " => " ++ format c))
instance [ToFormat α] : ToFormat (Trie α) := ⟨Trie.format⟩
instance [ToFormat α] : ToFormat (Trie α s) := ⟨Trie.format⟩
partial def format [ToFormat α] (d : DiscrTree α) : Format :=
partial def format [ToFormat α] (d : DiscrTree α s) : Format :=
let (_, r) := d.root.foldl
(fun (p : Bool × Format) k c =>
(false, p.2 ++ (if p.1 then Format.nil else Format.line) ++ Format.paren (Std.format k ++ " => " ++ Std.format c)))
(true, Format.nil)
Format.group r
instance [ToFormat α] : ToFormat (DiscrTree α) := ⟨format⟩
instance [ToFormat α] : ToFormat (DiscrTree α s) := ⟨format⟩
/-- The discrimination tree ignores implicit arguments and proofs.
We use the following auxiliary id as a "mark". -/
private def tmpMVarId : MVarId := { name := `_discr_tree_tmp }
private def tmpStar := mkMVar tmpMVarId
instance : Inhabited (DiscrTree α) where
instance : Inhabited (DiscrTree α s) where
default := {}
/--
@ -240,12 +240,12 @@ we could not even compile `Init` with this setup.
Remark: rnote it is not sufficient to just unfold reducible definitions and perform
beta-reduction, we must also instantiate assgined metavariables, and perform zeta-reduction.
-/
partial def reduce (e : Expr) : MetaM Expr := do
let e ← whnfCore e (iota := false)
partial def reduce (e : Expr) (simpleReduce : Bool) : MetaM Expr := do
let e ← whnfCore e (iota := !simpleReduce)
match (← unfoldDefinition? e) with
| some e => reduce e
| some e => reduce e simpleReduce
| none => match e.etaExpandedStrict? with
| some e => reduce e
| some e => reduce e simpleReduce
| none => return e
/--
@ -280,18 +280,18 @@ where
| none => return e
/-- whnf for the discrimination tree module -/
def reduceDT (e : Expr) (root : Bool) : MetaM Expr :=
if root then reduceUntilBadKey e else reduce e
def reduceDT (e : Expr) (root : Bool) (simpleReduce : Bool) : MetaM Expr :=
if root then reduceUntilBadKey e else reduce e simpleReduce
/- Remark: we use `shouldAddAsStar` only for nested terms, and `root == false` for nested terms -/
private def pushArgs (root : Bool) (todo : Array Expr) (e : Expr) : MetaM (Key × Array Expr) := do
private def pushArgs (root : Bool) (todo : Array Expr) (e : Expr) : MetaM (Key s × Array Expr) := do
if hasNoindexAnnotation e then
return (.star, todo)
else
let e ← reduceDT e root
let e ← reduceDT e root (simpleReduce := s)
let fn := e.getAppFn
let push (k : Key) (nargs : Nat) : MetaM (Key × Array Expr) := do
let push (k : Key s) (nargs : Nat) : MetaM (Key s × Array Expr) := do
let info ← getFunInfoNArgs fn nargs
let todo ← pushArgsAux info.paramInfo (nargs-1) e todo
return (k, todo)
@ -324,7 +324,7 @@ private def pushArgs (root : Bool) (todo : Array Expr) (e : Expr) : MetaM (Key
| _ =>
return (.other, todo)
partial def mkPathAux (root : Bool) (todo : Array Expr) (keys : Array Key) : MetaM (Array Key) := do
partial def mkPathAux (root : Bool) (todo : Array Expr) (keys : Array (Key s)) : MetaM (Array (Key s)) := do
if todo.isEmpty then
return keys
else
@ -335,13 +335,13 @@ partial def mkPathAux (root : Bool) (todo : Array Expr) (keys : Array Key) : Met
private def initCapacity := 8
def mkPath (e : Expr) : MetaM (Array Key) := do
def mkPath (e : Expr) : MetaM (Array (Key s)) := do
withReducible do
let todo : Array Expr := .mkEmpty initCapacity
let keys : Array Key := .mkEmpty initCapacity
let keys : Array (Key s) := .mkEmpty initCapacity
mkPathAux (root := true) (todo.push e) keys
private partial def createNodes (keys : Array Key) (v : α) (i : Nat) : Trie α :=
private partial def createNodes (keys : Array (Key s)) (v : α) (i : Nat) : Trie α s :=
if h : i < keys.size then
let k := keys.get ⟨i, h⟩
let c := createNodes keys v (i+1)
@ -352,7 +352,7 @@ private partial def createNodes (keys : Array Key) (v : α) (i : Nat) : Trie α
private def insertVal [BEq α] (vs : Array α) (v : α) : Array α :=
if vs.contains v then vs else vs.push v
private partial def insertAux [BEq α] (keys : Array Key) (v : α) : Nat → Trie α → Trie α
private partial def insertAux [BEq α] (keys : Array (Key s)) (v : α) : Nat → Trie α s → Trie α s
| i, .node vs cs =>
if h : i < keys.size then
let k := keys.get ⟨i, h⟩
@ -365,7 +365,7 @@ private partial def insertAux [BEq α] (keys : Array Key) (v : α) : Nat → Tri
else
.node (insertVal vs v) cs
def insertCore [BEq α] (d : DiscrTree α) (keys : Array Key) (v : α) : DiscrTree α :=
def insertCore [BEq α] (d : DiscrTree α s) (keys : Array (Key s)) (v : α) : DiscrTree α s :=
if keys.isEmpty then panic! "invalid key sequence"
else
let k := keys[0]!
@ -377,12 +377,12 @@ def insertCore [BEq α] (d : DiscrTree α) (keys : Array Key) (v : α) : DiscrTr
let c := insertAux keys v 1 c
{ root := d.root.insert k c }
def insert [BEq α] (d : DiscrTree α) (e : Expr) (v : α) : MetaM (DiscrTree α) := do
def insert [BEq α] (d : DiscrTree α s) (e : Expr) (v : α) : MetaM (DiscrTree α s) := do
let keys ← mkPath e
return d.insertCore keys v
private def getKeyArgs (e : Expr) (isMatch root : Bool) : MetaM (Key × Array Expr) := do
let e ← reduceDT e root
private def getKeyArgs (e : Expr) (isMatch root : Bool) : MetaM (Key s × Array Expr) := do
let e ← reduceDT e root (simpleReduce := s)
match e.getAppFn with
| .lit v => return (.lit v, #[])
| .const c _ =>
@ -454,22 +454,22 @@ private def getKeyArgs (e : Expr) (isMatch root : Bool) : MetaM (Key × Array Ex
| _ =>
return (.other, #[])
private abbrev getMatchKeyArgs (e : Expr) (root : Bool) : MetaM (Key × Array Expr) :=
private abbrev getMatchKeyArgs (e : Expr) (root : Bool) : MetaM (Key s × Array Expr) :=
getKeyArgs e (isMatch := true) (root := root)
private abbrev getUnifyKeyArgs (e : Expr) (root : Bool) : MetaM (Key × Array Expr) :=
private abbrev getUnifyKeyArgs (e : Expr) (root : Bool) : MetaM (Key s × Array Expr) :=
getKeyArgs e (isMatch := false) (root := root)
private def getStarResult (d : DiscrTree α) : Array α :=
private def getStarResult (d : DiscrTree α s) : Array α :=
let result : Array α := .mkEmpty initCapacity
match d.root.find? .star with
| none => result
| some (.node vs _) => result ++ vs
private abbrev findKey (cs : Array (Key × Trie α)) (k : Key) : Option (Key × Trie α) :=
private abbrev findKey (cs : Array (Key s × Trie α s)) (k : Key s) : Option (Key s × Trie α s) :=
cs.binSearch (k, default) (fun a b => a.1 < b.1)
private partial def getMatchLoop (todo : Array Expr) (c : Trie α) (result : Array α) : MetaM (Array α) := do
private partial def getMatchLoop (todo : Array Expr) (c : Trie α s) (result : Array α) : MetaM (Array α) := do
match c with
| .node vs cs =>
if todo.isEmpty then
@ -489,7 +489,7 @@ private partial def getMatchLoop (todo : Array Expr) (c : Trie α) (result : Arr
getMatchLoop todo first.2 result
else
return result
let visitNonStar (k : Key) (args : Array Expr) (result : Array α) : MetaM (Array α) :=
let visitNonStar (k : Key s) (args : Array Expr) (result : Array α) : MetaM (Array α) :=
match findKey cs k with
| none => return result
| some c => getMatchLoop (todo ++ args) c.2 result
@ -504,12 +504,12 @@ private partial def getMatchLoop (todo : Array Expr) (c : Trie α) (result : Arr
| .arrow => visitNonStar .other #[] (← visitNonStar k args result)
| _ => visitNonStar k args result
private def getMatchRoot (d : DiscrTree α) (k : Key) (args : Array Expr) (result : Array α) : MetaM (Array α) :=
private def getMatchRoot (d : DiscrTree α s) (k : Key s) (args : Array Expr) (result : Array α) : MetaM (Array α) :=
match d.root.find? k with
| none => return result
| some c => getMatchLoop args c result
private def getMatchCore (d : DiscrTree α) (e : Expr) : MetaM (Key × Array α) :=
private def getMatchCore (d : DiscrTree α s) (e : Expr) : MetaM (Key s × Array α) :=
withReducible do
let result := getStarResult d
let (k, args) ← getMatchKeyArgs e (root := true)
@ -522,13 +522,13 @@ private def getMatchCore (d : DiscrTree α) (e : Expr) : MetaM (Key × Array α)
/--
Find values that match `e` in `d`.
-/
def getMatch (d : DiscrTree α) (e : Expr) : MetaM (Array α) :=
def getMatch (d : DiscrTree α s) (e : Expr) : MetaM (Array α) :=
return (← getMatchCore d e).2
/--
Similar to `getMatch`, but returns solutions that are prefixes of `e`.
We store the number of ignored arguments in the result.-/
partial def getMatchWithExtra (d : DiscrTree α) (e : Expr) : MetaM (Array (α × Nat)) := do
partial def getMatchWithExtra (d : DiscrTree α s) (e : Expr) : MetaM (Array (α × Nat)) := do
let (k, result) ← getMatchCore d e
let result := result.map (·, 0)
if !e.isApp then
@ -538,8 +538,8 @@ partial def getMatchWithExtra (d : DiscrTree α) (e : Expr) : MetaM (Array (α
else
go e.appFn! 1 result
where
mayMatchPrefix (k : Key) : MetaM Bool :=
let cont (k : Key) : MetaM Bool :=
mayMatchPrefix (k : Key s) : MetaM Bool :=
let cont (k : Key s) : MetaM Bool :=
if d.root.find? k |>.isSome then
return true
else
@ -556,7 +556,7 @@ where
else
return result
partial def getUnify (d : DiscrTree α) (e : Expr) : MetaM (Array α) :=
partial def getUnify (d : DiscrTree α s) (e : Expr) : MetaM (Array α) :=
withReducible do
let (k, args) ← getUnifyKeyArgs e (root := true)
match k with
@ -567,7 +567,7 @@ partial def getUnify (d : DiscrTree α) (e : Expr) : MetaM (Array α) :=
| none => return result
| some c => process 0 args c result
where
process (skip : Nat) (todo : Array Expr) (c : Trie α) (result : Array α) : MetaM (Array α) := do
process (skip : Nat) (todo : Array Expr) (c : Trie α s) (result : Array α) : MetaM (Array α) := do
match skip, c with
| skip+1, .node _ cs =>
if cs.isEmpty then
@ -589,7 +589,7 @@ where
process 0 todo first.2 result
else
return result
let visitNonStar (k : Key) (args : Array Expr) (result : Array α) : MetaM (Array α) :=
let visitNonStar (k : Key s) (args : Array Expr) (result : Array α) : MetaM (Array α) :=
match findKey cs k with
| none => return result
| some c => process 0 (todo ++ args) c.2 result

71
src/Lean/Meta/DiscrTreeTypes.lean
View file

@ -10,18 +10,20 @@ namespace Lean.Meta
/-! See file `DiscrTree.lean` for the actual implementation and documentation. -/
namespace DiscrTree
inductive Key where
| const : Name → Nat → Key
| fvar : FVarId → Nat → Key
| lit : Literal → Key
| star : Key
| other : Key
| arrow : Key
| proj : Name → Nat → Key
/--
Discrimination tree key. See `DiscrTree`
-/
inductive Key (simpleReduce : Bool) where
| const : Name → Nat → Key simpleReduce
| fvar : FVarId → Nat → Key simpleReduce
| lit : Literal → Key simpleReduce
| star : Key simpleReduce
| other : Key simpleReduce
| arrow : Key simpleReduce
| proj : Name → Nat → Key simpleReduce
deriving Inhabited, BEq, Repr
protected def Key.hash : Key → UInt64
protected def Key.hash : Key s → UInt64
| Key.const n a => mixHash 5237 $ mixHash (hash n) (hash a)
| Key.fvar n a => mixHash 3541 $ mixHash (hash n) (hash a)
| Key.lit v => mixHash 1879 $ hash v
@ -30,16 +32,55 @@ protected def Key.hash : Key → UInt64
| Key.arrow => 17
| Key.proj s i => mixHash 11 $ mixHash (hash s) (hash i)
instance : Hashable Key := ⟨Key.hash⟩
instance : Hashable (Key s) := ⟨Key.hash⟩
inductive Trie (α : Type) where
| node (vs : Array α) (children : Array (Key × Trie α)) : Trie α
/--
Discrimination tree trie. See `DiscrTree`.
-/
inductive Trie (α : Type) (simpleReduce : Bool) where
| node (vs : Array α) (children : Array (Key simpleReduce × Trie α simpleReduce)) : Trie α simpleReduce
end DiscrTree
open DiscrTree
structure DiscrTree (α : Type) where
root : PersistentHashMap Key (Trie α) := {}
/--
Discrimination trees. It is an index from terms to values of type `α`.
If `simpleReduce := true`, then only simple reduction are performed while
indexing/retrieving terms. For example, `iota` reduction is not performed.
We use `simpleReduce := false` in the type class resolution module,
and `simpleReduce := true` in `simp`.
Motivations:
- In `simp`, we want to have `simp` theorem such as
```
@[simp] theorem liftOn_mk (a : α) (f : α → γ) (h : ∀ a₁ a₂, r a₁ a₂ → f a₁ = f a₂) :
Quot.liftOn (Quot.mk r a) f h = f a := rfl
```
If we enable `iota`, then the lhs is reduced to `f a`.
- During type class resolution, we often want to reduce types using even `iota`.
Example:
```
inductive Ty where
| int
| bool
@[reducible] def Ty.interp (ty : Ty) : Type :=
Ty.casesOn (motive := fun _ => Type) ty Int Bool
def test {a b c : Ty} (f : a.interp → b.interp → c.interp) (x : a.interp) (y : b.interp) : c.interp :=
f x y
def f (a b : Ty.bool.interp) : Ty.bool.interp :=
-- We want to synthesize `BEq Ty.bool.interp` here, and it will fail
-- if we do not reduce `Ty.bool.interp` to `Bool`.
test (.==.) a b
```
-/
structure DiscrTree (α : Type) (simpleReduce : Bool) where
root : PersistentHashMap (Key simpleReduce) (Trie α simpleReduce) := {}
end Lean.Meta

34
src/Lean/Meta/Instances.lean
View file

@ -9,8 +9,32 @@ import Lean.Meta.DiscrTree
namespace Lean.Meta
/-
Note: we want to use iota reduction when indexing instaces. Otherwise,
we cannot elaborate examples such as
```
inductive Ty where
| int
| bool
@[reducible] def Ty.interp (ty : Ty) : Type :=
Ty.casesOn (motive := fun _ => Type) ty Int Bool
def test {a b c : Ty} (f : a.interp → b.interp → c.interp) (x : a.interp) (y : b.interp) : c.interp :=
f x y
def f (a b : Ty.bool.interp) : Ty.bool.interp :=
-- We want to synthesize `BEq Ty.bool.interp` here, and it will fail
-- if we do not reduce `Ty.bool.interp` to `Bool`.
test (.==.) a b
```
See comment at `DiscrTree`.
-/
abbrev InstanceKey := DiscrTree.Key (simpleReduce := false)
structure InstanceEntry where
keys : Array DiscrTree.Key
keys : Array InstanceKey
val : Expr
priority : Nat
globalName? : Option Name := none
@ -24,8 +48,10 @@ instance : ToFormat InstanceEntry where
| some n => format n
| _ => "<local>"
abbrev InstanceTree := DiscrTree InstanceEntry (simpleReduce := false)
structure Instances where
discrTree : DiscrTree InstanceEntry := DiscrTree.empty
discrTree : InstanceTree := DiscrTree.empty
instanceNames : PHashSet Name := {}
erased : PHashSet Name := {}
deriving Inhabited
@ -49,7 +75,7 @@ builtin_initialize instanceExtension : SimpleScopedEnvExtension InstanceEntry In
addEntry := addInstanceEntry
}
private def mkInstanceKey (e : Expr) : MetaM (Array DiscrTree.Key) := do
private def mkInstanceKey (e : Expr) : MetaM (Array InstanceKey) := do
let type ← inferType e
withNewMCtxDepth do
let (_, _, type) ← forallMetaTelescopeReducing type
@ -74,7 +100,7 @@ builtin_initialize
modifyEnv fun env => instanceExtension.modifyState env fun _ => s
}
def getGlobalInstancesIndex : CoreM (DiscrTree InstanceEntry) :=
def getGlobalInstancesIndex : CoreM (DiscrTree InstanceEntry (simpleReduce := false)) :=
return Meta.instanceExtension.getState (← getEnv) |>.discrTree
def getErasedInstances : CoreM (PHashSet Name) :=

2
src/Lean/Meta/Tactic/Simp/Rewrite.lean
View file

@ -134,7 +134,7 @@ def tryTheorem? (e : Expr) (thm : SimpTheorem) (discharge? : Expr → SimpM (Opt
/--
Remark: the parameter tag is used for creating trace messages. It is irrelevant otherwise.
-/
def rewrite? (e : Expr) (s : DiscrTree SimpTheorem) (erased : PHashSet Origin) (discharge? : Expr → SimpM (Option Expr)) (tag : String) (rflOnly : Bool) : SimpM (Option Result) := do
def rewrite? (e : Expr) (s : SimpTheoremTree) (erased : PHashSet Origin) (discharge? : Expr → SimpM (Option Expr)) (tag : String) (rflOnly : Bool) : SimpM (Option Result) := do
let candidates ← s.getMatchWithExtra e
if candidates.isEmpty then
trace[Debug.Meta.Tactic.simp] "no theorems found for {tag}-rewriting {e}"

23
src/Lean/Meta/Tactic/Simp/SimpTheorems.lean
View file

@ -50,6 +50,19 @@ def Origin.key : Origin → Name
instance : BEq Origin := ⟨(·.key == ·.key)⟩
instance : Hashable Origin := ⟨(hash ·.key)⟩
/-
Note: we want to use iota reduction when indexing instaces. Otherwise,
we cannot use simp theorems such as
```
@[simp] theorem liftOn_mk (a : α) (f : α → γ) (h : ∀ a₁ a₂, r a₁ a₂ → f a₁ = f a₂) :
Quot.liftOn (Quot.mk r a) f h = f a := rfl
```
If we use `iota`, then the lhs is reduced to `f a`.
See comment at `DiscrTree`.
-/
abbrev SimpTheoremKey := DiscrTree.Key (simpleReduce := true)
/--
The fields `levelParams` and `proof` are used to encode the proof of the simp theorem.
If the `proof` is a global declaration `c`, we store `Expr.const c []` at `proof` without the universe levels, and `levelParams` is set to `#[]`
@ -60,7 +73,7 @@ instance : Hashable Origin := ⟨(hash ·.key)⟩
Then, we use `abstractMVars` to abstract the universe metavariables and create new fresh universe parameters that are stored at the field `levelParams`.
-/
structure SimpTheorem where
keys : Array DiscrTree.Key := #[]
keys : Array SimpTheoremKey := #[]
/--
It stores universe parameter names for universe polymorphic proofs.
Recall that it is non-empty only when we elaborate an expression provided by the user.
@ -137,9 +150,11 @@ def ppSimpTheorem [Monad m] [MonadLiftT IO m] [MonadEnv m] [MonadError m] (s : S
instance : BEq SimpTheorem where
beq e₁ e₂ := e₁.proof == e₂.proof
abbrev SimpTheoremTree := DiscrTree SimpTheorem (simpleReduce := true)
structure SimpTheorems where
pre : DiscrTree SimpTheorem := DiscrTree.empty
post : DiscrTree SimpTheorem := DiscrTree.empty
pre : SimpTheoremTree := DiscrTree.empty
post : SimpTheoremTree := DiscrTree.empty
lemmaNames : PHashSet Origin := {}
toUnfold : PHashSet Name := {}
erased : PHashSet Origin := {}
@ -202,7 +217,7 @@ private partial def isPerm : Expr → Expr → MetaM Bool
| s, t => return s == t
private def checkBadRewrite (lhs rhs : Expr) : MetaM Unit := do
let lhs ← DiscrTree.reduceDT lhs (root := true)
let lhs ← DiscrTree.reduceDT lhs (root := true) (simpleReduce := true)
if lhs == rhs && lhs.isFVar then
throwError "invalid `simp` theorem, equation is equivalent to{indentExpr (← mkEq lhs rhs)}"

8
src/Lean/Meta/UnificationHint.lean
View file

@ -10,13 +10,17 @@ import Lean.Meta.SynthInstance
namespace Lean.Meta
abbrev UnificationHintKey := DiscrTree.Key (simpleReduce := true)
structure UnificationHintEntry where
keys : Array DiscrTree.Key
keys : Array UnificationHintKey
val : Name
deriving Inhabited
abbrev UnificationHintTree := DiscrTree Name (simpleReduce := true)
structure UnificationHints where
discrTree : DiscrTree Name := DiscrTree.empty
discrTree : UnificationHintTree := DiscrTree.empty
deriving Inhabited
instance : ToFormat UnificationHints where

2
tests/lean/run/meta3.lean
View file

@ -32,7 +32,7 @@ def succ := mkConst `Nat.succ
def add := mkAppN (mkConst `Add.add [levelZero]) #[nat, mkConst `Nat.add]
def tst1 : MetaM Unit :=
do let d : DiscrTree Nat := {};
do let d : DiscrTree Nat true := {};
let mvar ← mkFreshExprMVar nat;
let d ← d.insert (mkAppN add #[mvar, mkNatLit 10]) 1;
let d ← d.insert (mkAppN add #[mkNatLit 0, mkNatLit 10]) 2;

6
tests/lean/run/stuckTC.lean
View file

@ -45,6 +45,12 @@ inductive Ty where
@[reducible] def Ty.interp (ty : Ty) : Type :=
Ty.casesOn (motive := fun _ => Type) ty Int Bool
/-
The discrimination tree module does not perform iota reduction. Thus, it does
not reduce the definition above, and we cannot synthesize `BEq Ty.bool.interp`.
We can workaround using `match` as in the ex
-/
def test {a b c : Ty} (f : a.interp → b.interp → c.interp) (x : a.interp) (y : b.interp) : c.interp :=
f x y