Equations
- Lean.Meta.DiscrTree.Key.ctorIdx x = match x with | Lean.Meta.DiscrTree.Key.star => 0 | Lean.Meta.DiscrTree.Key.other => 1 | Lean.Meta.DiscrTree.Key.lit x => 2 | Lean.Meta.DiscrTree.Key.fvar x x_1 => 3 | Lean.Meta.DiscrTree.Key.const x x_1 => 4 | Lean.Meta.DiscrTree.Key.arrow => 5 | Lean.Meta.DiscrTree.Key.proj x x_1 => 6
Equations
- Lean.Meta.DiscrTree.Key.lt x x = match x, x with | Lean.Meta.DiscrTree.Key.lit v₁, Lean.Meta.DiscrTree.Key.lit v₂ => decide (v₁ < v₂) | Lean.Meta.DiscrTree.Key.fvar n₁ a₁, Lean.Meta.DiscrTree.Key.fvar n₂ a₂ => Lean.Name.quickLt n₁.name n₂.name || n₁ == n₂ && decide (a₁ < a₂) | Lean.Meta.DiscrTree.Key.const n₁ a₁, Lean.Meta.DiscrTree.Key.const n₂ a₂ => Lean.Name.quickLt n₁ n₂ || n₁ == n₂ && decide (a₁ < a₂) | Lean.Meta.DiscrTree.Key.proj s₁ i₁, Lean.Meta.DiscrTree.Key.proj s₂ i₂ => Lean.Name.quickLt s₁ s₂ || s₁ == s₂ && decide (i₁ < i₂) | k₁, k₂ => decide (Lean.Meta.DiscrTree.Key.ctorIdx k₁ < Lean.Meta.DiscrTree.Key.ctorIdx k₂)
Equations
- Lean.Meta.DiscrTree.instLTKey = { lt := fun a b => Lean.Meta.DiscrTree.Key.lt a b = true }
instance
Lean.Meta.DiscrTree.instDecidableLtKeyInstLTKey
(a : Lean.Meta.DiscrTree.Key)
(b : Lean.Meta.DiscrTree.Key)
:
Equations
Equations
- Lean.Meta.DiscrTree.Key.format x = match x with | Lean.Meta.DiscrTree.Key.star => Std.Format.text "*" | Lean.Meta.DiscrTree.Key.other => Std.Format.text "◾" | Lean.Meta.DiscrTree.Key.lit (Lean.Literal.natVal v) => Lean.format v | Lean.Meta.DiscrTree.Key.lit (Lean.Literal.strVal v) => repr v | Lean.Meta.DiscrTree.Key.const k x => Lean.format k | Lean.Meta.DiscrTree.Key.proj s i => Lean.format s ++ Std.Format.text "." ++ Lean.format i | Lean.Meta.DiscrTree.Key.fvar k x => Lean.format k.name | Lean.Meta.DiscrTree.Key.arrow => Std.Format.text "→"
Equations
Equations
- Lean.Meta.DiscrTree.Key.arity x = match x with | Lean.Meta.DiscrTree.Key.const x a => a | Lean.Meta.DiscrTree.Key.fvar x a => a | Lean.Meta.DiscrTree.Key.arrow => 2 | Lean.Meta.DiscrTree.Key.proj x x_1 => 1 | x => 0
Equations
- Lean.Meta.DiscrTree.instInhabitedTrie = { default := Lean.Meta.DiscrTree.Trie.node #[] #[] }
Equations
- Lean.Meta.DiscrTree.empty = { root := { root := Std.PersistentHashMap.Node.entries Std.PersistentHashMap.mkEmptyEntriesArray, size := 0 } }
Equations
- Lean.Meta.DiscrTree.instToFormatTrie = { format := Lean.Meta.DiscrTree.Trie.format }
Equations
- Lean.Meta.DiscrTree.format d = let x := Std.PersistentHashMap.foldl d.root (fun p k c => (false, (p.snd ++ if p.fst = true then Lean.Format.nil else Lean.Format.line) ++ Lean.Format.paren (Lean.format k ++ Std.Format.text " => " ++ Lean.format c))) (true, Lean.Format.nil); match x with | (x, r) => Lean.Format.group r
Equations
- Lean.Meta.DiscrTree.instToFormatDiscrTree = { format := Lean.Meta.DiscrTree.format }
Equations
- Lean.Meta.DiscrTree.instInhabitedDiscrTree = { default := { root := { root := Std.PersistentHashMap.Node.entries Std.PersistentHashMap.mkEmptyEntriesArray, size := 0 } } }
Equations
- Lean.Meta.DiscrTree.mkNoindexAnnotation e = Lean.mkAnnotation `noindex e
Equations
- Lean.Meta.DiscrTree.hasNoindexAnnotation e = Option.isSome (Lean.annotation? `noindex e)
Equations
- Lean.Meta.DiscrTree.whnfDT e root = if root = true then Lean.Meta.DiscrTree.whnfUntilBadKey e else Lean.Meta.DiscrTree.whnfEta e
partial def
Lean.Meta.DiscrTree.mkPathAux
(root : Bool)
(todo : Array Lean.Expr)
(keys : Array Lean.Meta.DiscrTree.Key)
:
Equations
- Lean.Meta.DiscrTree.mkPath e = Lean.Meta.withReducible (let todo := Array.mkEmpty Lean.Meta.DiscrTree.initCapacity; let keys := Array.mkEmpty Lean.Meta.DiscrTree.initCapacity; Lean.Meta.DiscrTree.mkPathAux true (Array.push todo e) keys)
def
Lean.Meta.DiscrTree.insertCore
{α : Type}
[inst : BEq α]
(d : Lean.Meta.DiscrTree α)
(keys : Array Lean.Meta.DiscrTree.Key)
(v : α)
:
Equations
- Lean.Meta.DiscrTree.insertCore d keys v = if Array.isEmpty keys = true then panicWithPosWithDecl "Lean.Meta.DiscrTree" "Lean.Meta.DiscrTree.insertCore" 352 23 "invalid key sequence" else let k := Array.getOp keys 0; match Std.PersistentHashMap.find? d.root k with | none => let c := Lean.Meta.DiscrTree.createNodes keys v 1; { root := Std.PersistentHashMap.insert d.root k c } | some c => let c := Lean.Meta.DiscrTree.insertAux keys v 1 c; { root := Std.PersistentHashMap.insert d.root k c }
def
Lean.Meta.DiscrTree.insert
{α : Type}
[inst : BEq α]
(d : Lean.Meta.DiscrTree α)
(e : Lean.Expr)
(v : α)
:
Equations
- Lean.Meta.DiscrTree.insert d e v = do let keys ← Lean.Meta.DiscrTree.mkPath e pure (Lean.Meta.DiscrTree.insertCore d keys v)
def
Lean.Meta.DiscrTree.getMatch
{α : Type}
(d : Lean.Meta.DiscrTree α)
(e : Lean.Expr)
:
Lean.MetaM (Array α)
Equations
- Lean.Meta.DiscrTree.getMatch d e = Lean.Meta.withReducible (let result := Lean.Meta.DiscrTree.getStarResult d; do let discr ← Lean.Meta.DiscrTree.getMatchKeyArgs e true let x : Lean.Meta.DiscrTree.Key × Array Lean.Expr := discr match x with | (k, args) => match k with | Lean.Meta.DiscrTree.Key.star => pure result | x => Lean.Meta.DiscrTree.getMatchRoot d k args result)
def
Lean.Meta.DiscrTree.getMatchWithExtra
{α : Type}
(d : Lean.Meta.DiscrTree α)
(e : Lean.Expr)
:
Lean.MetaM (Array (α × Nat))
Equations
- Lean.Meta.DiscrTree.getMatchWithExtra d e = (fun process => Lean.Meta.withReducible (let result := Array.map (fun a => (a, 0)) (Lean.Meta.DiscrTree.getStarResult d); do let discr ← Lean.Meta.DiscrTree.getMatchKeyArgs e true let x : Lean.Meta.DiscrTree.Key × Array Lean.Expr := discr match x with | (k, args) => match k with | Lean.Meta.DiscrTree.Key.star => pure result | x => process k (Array.toSubarray args 0 (Array.size args)) 0 result)) (Lean.Meta.DiscrTree.getMatchWithExtra.process d)
partial def
Lean.Meta.DiscrTree.getMatchWithExtra.process
{α : Type}
(d : Lean.Meta.DiscrTree α)
(k : Lean.Meta.DiscrTree.Key)
(args : Subarray Lean.Expr)
(numExtraArgs : Nat)
(result : Array (α × Nat))
:
Lean.MetaM (Array (α × Nat))
def
Lean.Meta.DiscrTree.getUnify
{α : Type}
(d : Lean.Meta.DiscrTree α)
(e : Lean.Expr)
:
Lean.MetaM (Array α)
Equations
- Lean.Meta.DiscrTree.getUnify d e = (fun process => Lean.Meta.withReducible do let discr ← Lean.Meta.DiscrTree.getUnifyKeyArgs e true let x : Lean.Meta.DiscrTree.Key × Array Lean.Expr := discr match x with | (k, args) => match k with | Lean.Meta.DiscrTree.Key.star => Std.PersistentHashMap.foldlM d.root (fun result k c => process (Lean.Meta.DiscrTree.Key.arity k) #[] c result) #[] | x => let result := Lean.Meta.DiscrTree.getStarResult d; match Std.PersistentHashMap.find? d.root k with | none => pure result | some c => process 0 args c result) Lean.Meta.DiscrTree.getUnify.process
partial def
Lean.Meta.DiscrTree.getUnify.process
{α : Type}
(skip : Nat)
(todo : Array Lean.Expr)
(c : Lean.Meta.DiscrTree.Trie α)
(result : Array α)
:
Lean.MetaM (Array α)