Built with doc-gen4, running Lean4. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑Ctrl+↓to navigate, Ctrl+πŸ–±οΈto focus. On Mac, use Cmdinstead of Ctrl. 
/-
Copyright (c) 2022 Jannis Limperg. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Jannis Limperg
-/

import Lean.Meta.DiscrTree
import Std.Data.Array.Merge
import Std.Data.Ord
import Std.Lean.Meta.Expr
import Std.Lean.PersistentHashMap

namespace Lean.Meta.DiscrTree

namespace Key

/--
Compare two `Key`s. The ordering is total but otherwise arbitrary. (It uses
`Name.quickCmp` internally.)
-/
protected def 
cmp: {s : Bool} β†’ Key s β†’ Key s β†’ Ordering
cmp : 
Key: Bool β†’ Type
Key 
s: ?m.4
s β†’ 
Key: Bool β†’ Type
Key 
s: ?m.4
s β†’ 
Ordering: Type
Ordering
  | 
.lit: {simpleReduce : Bool} β†’ Literal β†’ Key simpleReduce
.lit 
v₁: Literal
v₁,        
.lit: {simpleReduce : Bool} β†’ Literal β†’ Key simpleReduce
.lit 
vβ‚‚: Literal
vβ‚‚        => 
compare: {Ξ± : Type ?u.40} β†’ [self : Ord Ξ±] β†’ Ξ± β†’ Ξ± β†’ Ordering
compare 
v₁: Literal
v₁ 
vβ‚‚: Literal
vβ‚‚
  | 
.fvar: {simpleReduce : Bool} β†’ FVarId β†’ Nat β†’ Key simpleReduce
.fvar 
n₁: FVarId
n₁ 
a₁: Nat
a₁,    
.fvar: {simpleReduce : Bool} β†’ FVarId β†’ Nat β†’ Key simpleReduce
.fvar 
nβ‚‚: FVarId
nβ‚‚ 
aβ‚‚: Nat
aβ‚‚    => 
n₁: FVarId
n₁.
name: FVarId β†’ Name
name.
quickCmp: Name β†’ Name β†’ Ordering
quickCmp 
nβ‚‚: FVarId
nβ‚‚.
name: FVarId β†’ Name
name |>.
then: Ordering β†’ Ordering β†’ Ordering
then <| 
compare: {Ξ± : Type ?u.81} β†’ [self : Ord Ξ±] β†’ Ξ± β†’ Ξ± β†’ Ordering
compare 
a₁: Nat
a₁ 
aβ‚‚: Nat
aβ‚‚
  | 
.const: {simpleReduce : Bool} β†’ Name β†’ Nat β†’ Key simpleReduce
.const 
n₁: Name
n₁ 
a₁: Nat
a₁,   
.const: {simpleReduce : Bool} β†’ Name β†’ Nat β†’ Key simpleReduce
.const 
nβ‚‚: Name
nβ‚‚ 
aβ‚‚: Nat
aβ‚‚   => 
n₁: Name
n₁.
quickCmp: Name β†’ Name β†’ Ordering
quickCmp 
nβ‚‚: Name
nβ‚‚ |>.
then: Ordering β†’ Ordering β†’ Ordering
then <| 
compare: {Ξ± : Type ?u.121} β†’ [self : Ord Ξ±] β†’ Ξ± β†’ Ξ± β†’ Ordering
compare 
a₁: Nat
a₁ 
aβ‚‚: Nat
aβ‚‚
  | 
.proj: {simpleReduce : Bool} β†’ Name β†’ Nat β†’ Nat β†’ Key simpleReduce
.proj 
s₁: Name
s₁ 
i₁: Nat
i₁ 
a₁: Nat
a₁, 
.proj: {simpleReduce : Bool} β†’ Name β†’ Nat β†’ Nat β†’ Key simpleReduce
.proj 
sβ‚‚: Name
sβ‚‚ 
iβ‚‚: Nat
iβ‚‚ 
aβ‚‚: Nat
aβ‚‚ =>
    
s₁: Name
s₁.
quickCmp: Name β†’ Name β†’ Ordering
quickCmp 
sβ‚‚: Name
sβ‚‚ |>.
then: Ordering β†’ Ordering β†’ Ordering
then <| 
compare: {Ξ± : Type ?u.170} β†’ [self : Ord Ξ±] β†’ Ξ± β†’ Ξ± β†’ Ordering
compare 
i₁: Nat
i₁ 
iβ‚‚: Nat
iβ‚‚ |>.
then: Ordering β†’ Ordering β†’ Ordering
then <| 
compare: {Ξ± : Type ?u.175} β†’ [self : Ord Ξ±] β†’ Ξ± β†’ Ξ± β†’ Ordering
compare 
a₁: Nat
a₁ 
aβ‚‚: Nat
aβ‚‚
  | 
k₁: Key s
k₁,             
kβ‚‚: Key s
kβ‚‚             => 
compare: {Ξ± : Type ?u.198} β†’ [self : Ord Ξ±] β†’ Ξ± β†’ Ξ± β†’ Ordering
compare 
k₁: Key s
k₁.
ctorIdx: {s : Bool} β†’ Key s β†’ Nat
ctorIdx 
kβ‚‚: Key s
kβ‚‚.
ctorIdx: {s : Bool} β†’ Key s β†’ Nat
ctorIdx


instance: {s : Bool} β†’ Ord (Key s)
instance : 
Ord: Type ?u.2092 β†’ Type ?u.2092
Ord (
Key: Bool β†’ Type
Key 
s: ?m.2089
s) :=
  ⟨
Key.cmp: {s : Bool} β†’ Key s β†’ Key s β†’ Ordering
Key.cmp⟩

end Key


namespace Trie

-- This is just a partial function, but Lean doesn't realise that its type is
-- inhabited.
private unsafe def 
foldMUnsafe: {m : Type u_1 β†’ Type u_2} β†’
  {s : Bool} β†’
    {Οƒ : Type u_1} β†’ {Ξ± : Type} β†’ [inst : Monad m] β†’ Array (Key s) β†’ (Οƒ β†’ Array (Key s) β†’ Ξ± β†’ m Οƒ) β†’ Οƒ β†’ Trie Ξ± s β†’ m Οƒ
foldMUnsafe [
Monad: (Type ?u.2168 β†’ Type ?u.2167) β†’ Type (max(?u.2168+1)?u.2167)
Monad 
m: ?m.2141
m] (
initialKeys: Array (Key s)
initialKeys : 
Array: Type ?u.2190 β†’ Type ?u.2190
Array (
Key: Bool β†’ Type
Key 
s: ?m.2151
s))
    (
f: Οƒ β†’ Array (Key s) β†’ Ξ± β†’ m Οƒ
f : 
Οƒ: ?m.2164
Οƒ β†’ 
Array: Type ?u.2196 β†’ Type ?u.2196
Array (
Key: Bool β†’ Type
Key 
s: ?m.2151
s) β†’ 
Ξ±: ?m.2182
Ξ± β†’ 
m: ?m.2141
m 
Οƒ: ?m.2164
Οƒ) (
init: Οƒ
init : 
Οƒ: ?m.2164
Οƒ) : 
Trie: Type β†’ Bool β†’ Type
Trie 
Ξ±: ?m.2182
Ξ± 
s: ?m.2151
s β†’ 
m: ?m.2141
m 
Οƒ: ?m.2164
Οƒ
  | 
Trie.node: {Ξ± : Type} β†’ {simpleReduce : Bool} β†’ Array Ξ± β†’ Array (Key simpleReduce Γ— Trie Ξ± simpleReduce) β†’ Trie Ξ± simpleReduce
Trie.node 
vs: Array Ξ±
vs 
children: Array (Key s Γ— Trie Ξ± s)
children => do
    let 
s: ?m.2349
s ← 
vs: Array Ξ±
vs.
foldlM: {Ξ± : Type ?u.2296} β†’
  {Ξ² : Type ?u.2295} β†’
    {m : Type ?u.2295 β†’ Type ?u.2294} β†’
      [inst : Monad m] β†’ (Ξ² β†’ Ξ± β†’ m Ξ²) β†’ Ξ² β†’ (as : Array Ξ±) β†’ optParam Nat 0 β†’ optParam Nat (Array.size as) β†’ m Ξ²
foldlM (init := 
init: Οƒ
init) fun 
s: ?m.2337
s 
v: ?m.2340
v => 
f: Οƒ β†’ Array (Key s✝) β†’ Ξ± β†’ m Οƒ
f 
s: ?m.2337
s 
initialKeys: Array (Key s✝)
initialKeys 
v: ?m.2340
v
    
children: Array (Key s✝ Γ— Trie Ξ± s✝)
children.
foldlM: {Ξ± : Type ?u.2353} β†’
  {Ξ² : Type ?u.2352} β†’
    {m : Type ?u.2352 β†’ Type ?u.2351} β†’
      [inst : Monad m] β†’ (Ξ² β†’ Ξ± β†’ m Ξ²) β†’ Ξ² β†’ (as : Array Ξ±) β†’ optParam Nat 0 β†’ optParam Nat (Array.size as) β†’ m Ξ²
foldlM (init := 
s: ?m.2349
s) fun 
s: ?m.2394
s (
k: Key s✝¹
k, 
t: Trie α s✝¹
t) =>
      
t: Trie α s✝¹
t.
foldMUnsafe: {m : Type ?u.2186 β†’ Type ?u.2185} β†’
  {s : Bool} β†’
    {Οƒ : Type ?u.2186} β†’
      {Ξ± : Type} β†’ [inst : Monad m] β†’ Array (Key s) β†’ (Οƒ β†’ Array (Key s) β†’ Ξ± β†’ m Οƒ) β†’ Οƒ β†’ Trie Ξ± s β†’ m Οƒ
foldMUnsafe (
initialKeys: Array (Key s✝¹)
initialKeys.
push: {Ξ± : Type ?u.2469} β†’ Array Ξ± β†’ Ξ± β†’ Array Ξ±
push 
k: Key s✝¹
k) 
f: Οƒ β†’ Array (Key s✝¹) β†’ Ξ± β†’ m Οƒ
f 
s: ?m.2394
s

/--
Monadically fold the keys and values stored in a `Trie`.
-/
@[implemented_by 
foldMUnsafe: {m : Type u_1 β†’ Type u_2} β†’
  {s : Bool} β†’
    {Οƒ : Type u_1} β†’ {Ξ± : Type} β†’ [inst : Monad m] β†’ Array (Key s) β†’ (Οƒ β†’ Array (Key s) β†’ Ξ± β†’ m Οƒ) β†’ Οƒ β†’ Trie Ξ± s β†’ m Οƒ
foldMUnsafe]
opaque 
foldM: {m : Type u_1 β†’ Type u_2} β†’
  {s : Bool} β†’
    {Οƒ : Type u_1} β†’ {Ξ± : Type} β†’ [inst : Monad m] β†’ Array (Key s) β†’ (Οƒ β†’ Array (Key s) β†’ Ξ± β†’ m Οƒ) β†’ Οƒ β†’ Trie Ξ± s β†’ m Οƒ
foldM [
Monad: (Type ?u.3045 β†’ Type ?u.3044) β†’ Type (max(?u.3045+1)?u.3044)
Monad 
m: ?m.3000
m] (
initalKeys: Array (Key s)
initalKeys : 
Array: Type ?u.3049 β†’ Type ?u.3049
Array (
Key: Bool β†’ Type
Key 
s: ?m.3010
s))
    (
f: Οƒ β†’ Array (Key s) β†’ Ξ± β†’ m Οƒ
f : 
Οƒ: ?m.3023
Οƒ β†’ 
Array: Type ?u.3055 β†’ Type ?u.3055
Array (
Key: Bool β†’ Type
Key 
s: ?m.3010
s) β†’ 
Ξ±: ?m.3041
Ξ± β†’ 
m: ?m.3000
m 
Οƒ: ?m.3023
Οƒ) (
init: Οƒ
init : 
Οƒ: ?m.3023
Οƒ) (
t: Trie Ξ± s
t : 
Trie: Type β†’ Bool β†’ Type
Trie 
Ξ±: ?m.3041
Ξ± 
s: ?m.3010
s) : 
m: ?m.3000
m 
Οƒ: ?m.3023
Οƒ :=
  
pure: {f : Type ?u.3076 β†’ Type ?u.3075} β†’ [self : Pure f] β†’ {Ξ± : Type ?u.3076} β†’ Ξ± β†’ f Ξ±
pure 
init: Οƒ
init

/--
Fold the keys and values stored in a `Trie`.
-/
@[inline]
def 
fold: {s : Bool} β†’ {Οƒ : Sort ?u.3228} β†’ {Ξ± : Type} β†’ Array (Key s) β†’ (Οƒ β†’ Array (Key s) β†’ Ξ± β†’ Οƒ) β†’ Οƒ β†’ Trie Ξ± s β†’ Οƒ
fold (
initialKeys: Array (Key s)
initialKeys : 
Array: Type ?u.3204 β†’ Type ?u.3204
Array (
Key: Bool β†’ Type
Key 
s: ?m.3201
s)) (
f: Οƒ β†’ Array (Key s) β†’ Ξ± β†’ Οƒ
f : 
Οƒ: ?m.3209
Οƒ β†’ 
Array: Type ?u.3231 β†’ Type ?u.3231
Array (
Key: Bool β†’ Type
Key 
s: ?m.3201
s) β†’ 
Ξ±: ?m.3222
Ξ± β†’ 
Οƒ: ?m.3209
Οƒ)
    (
init: Οƒ
init : 
Οƒ: ?m.3209
Οƒ) (
t: Trie Ξ± s
t : 
Trie: Type β†’ Bool β†’ Type
Trie 
Ξ±: ?m.3222
Ξ± 
s: ?m.3201
s) : 
Οƒ: ?m.3209
Οƒ :=
  
Id.run: {Ξ± : Type ?u.3249} β†’ Id Ξ± β†’ Ξ±
Id.run <| 
t: Trie Ξ± s
t.
foldM: {m : Type ?u.3252 β†’ Type ?u.3251} β†’
  {s : Bool} β†’
    {Οƒ : Type ?u.3252} β†’
      {Ξ± : Type} β†’ [inst : Monad m] β†’ Array (Key s) β†’ (Οƒ β†’ Array (Key s) β†’ Ξ± β†’ m Οƒ) β†’ Οƒ β†’ Trie Ξ± s β†’ m Οƒ
foldM 
initialKeys: Array (Key s)
initialKeys (init := 
init: Οƒ
init) fun 
s: ?m.3298
s 
k: ?m.3301
k 
a: ?m.3304
a => return 
f: Οƒ β†’ Array (Key s✝) β†’ Ξ± β†’ Οƒ
f 
s: ?m.3298
s 
k: ?m.3301
k 
a: ?m.3304
a

-- This is just a partial function, but Lean doesn't realise that its type is
-- inhabited.
private unsafe def 
foldValuesMUnsafe: {m : Type u_1 β†’ Type u_2} β†’
  {Οƒ : Type u_1} β†’ {Ξ± : Type} β†’ {s : Bool} β†’ [inst : Monad m] β†’ (Οƒ β†’ Ξ± β†’ m Οƒ) β†’ Οƒ β†’ Trie Ξ± s β†’ m Οƒ
foldValuesMUnsafe [
Monad: (Type ?u.3806 β†’ Type ?u.3805) β†’ Type (max(?u.3806+1)?u.3805)
Monad 
m: ?m.3780
m] (
f: Οƒ β†’ Ξ± β†’ m Οƒ
f : 
Οƒ: ?m.3790
Οƒ β†’ 
Ξ±: ?m.3802
Ξ± β†’ 
m: ?m.3780
m 
Οƒ: ?m.3790
Οƒ) (
init: Οƒ
init : 
Οƒ: ?m.3790
Οƒ) :
    
Trie: Type β†’ Bool β†’ Type
Trie 
Ξ±: ?m.3802
Ξ± 
s: ?m.3820
s β†’ 
m: ?m.3780
m 
Οƒ: ?m.3790
Οƒ
| 
node: {Ξ± : Type} β†’ {simpleReduce : Bool} β†’ Array Ξ± β†’ Array (Key simpleReduce Γ— Trie Ξ± simpleReduce) β†’ Trie Ξ± simpleReduce
node 
vs: Array Ξ±
vs 
children: Array (Key s Γ— Trie Ξ± s)
children => do
  let 
s: ?m.3976
s ← 
vs: Array Ξ±
vs.
foldlM: {Ξ± : Type ?u.3927} β†’
  {Ξ² : Type ?u.3926} β†’
    {m : Type ?u.3926 β†’ Type ?u.3925} β†’
      [inst : Monad m] β†’ (Ξ² β†’ Ξ± β†’ m Ξ²) β†’ Ξ² β†’ (as : Array Ξ±) β†’ optParam Nat 0 β†’ optParam Nat (Array.size as) β†’ m Ξ²
foldlM (init := 
init: Οƒ
init) 
f: Οƒ β†’ Ξ± β†’ m Οƒ
f
  
children: Array (Key s✝ Γ— Trie Ξ± s✝)
children.
foldlM: {Ξ± : Type ?u.3980} β†’
  {Ξ² : Type ?u.3979} β†’
    {m : Type ?u.3979 β†’ Type ?u.3978} β†’
      [inst : Monad m] β†’ (Ξ² β†’ Ξ± β†’ m Ξ²) β†’ Ξ² β†’ (as : Array Ξ±) β†’ optParam Nat 0 β†’ optParam Nat (Array.size as) β†’ m Ξ²
foldlM (init := 
s: ?m.3976
s) fun 
s: ?m.4021
s (_, 
c: Trie α s✝¹
c) => 
c: Trie α s✝¹
c.
foldValuesMUnsafe: {m : Type ?u.3824 β†’ Type ?u.3823} β†’
  {Οƒ : Type ?u.3824} β†’ {Ξ± : Type} β†’ {s : Bool} β†’ [inst : Monad m] β†’ (Οƒ β†’ Ξ± β†’ m Οƒ) β†’ Οƒ β†’ Trie Ξ± s β†’ m Οƒ
foldValuesMUnsafe (init := 
s: ?m.4021
s) 
f: Οƒ β†’ Ξ± β†’ m Οƒ
f

/--
Monadically fold the values stored in a `Trie`.
-/
@[implemented_by 
foldValuesMUnsafe: {m : Type u_1 β†’ Type u_2} β†’
  {Οƒ : Type u_1} β†’ {Ξ± : Type} β†’ {s : Bool} β†’ [inst : Monad m] β†’ (Οƒ β†’ Ξ± β†’ m Οƒ) β†’ Οƒ β†’ Trie Ξ± s β†’ m Οƒ
foldValuesMUnsafe]
opaque 
foldValuesM: {m : Type ?u.4572 β†’ Type ?u.4571} β†’
  {Οƒ : Type ?u.4572} β†’ {Ξ± : Type} β†’ {s : Bool} β†’ [inst : Monad m] β†’ (Οƒ β†’ Ξ± β†’ m Οƒ) β†’ Οƒ β†’ Trie Ξ± s β†’ m Οƒ
foldValuesM [
Monad: (Type ?u.4572 β†’ Type ?u.4571) β†’ Type (max(?u.4572+1)?u.4571)
Monad 
m: ?m.4529
m] (
f: Οƒ β†’ Ξ± β†’ m Οƒ
f : 
Οƒ: ?m.4539
Οƒ β†’ 
Ξ±: ?m.4551
Ξ± β†’ 
m: ?m.4529
m 
Οƒ: ?m.4539
Οƒ) (
init: Οƒ
init : 
Οƒ: ?m.4539
Οƒ) (
t: Trie Ξ± s
t : 
Trie: Type β†’ Bool β†’ Type
Trie 
Ξ±: ?m.4551
Ξ± 
s: ?m.4568
s) : 
m: ?m.4529
m 
Οƒ: ?m.4539
Οƒ := 
pure: {f : Type ?u.4596 β†’ Type ?u.4595} β†’ [self : Pure f] β†’ {Ξ± : Type ?u.4596} β†’ Ξ± β†’ f Ξ±
pure 
init: Οƒ
init

/--
Fold the values stored in a `Trie`.
-/
@[inline]
def 
foldValues: {Οƒ : Sort ?u.4733} β†’ {Ξ± : Type} β†’ {s : Bool} β†’ (Οƒ β†’ Ξ± β†’ Οƒ) β†’ Οƒ β†’ Trie Ξ± s β†’ Οƒ
foldValues (
f: Οƒ β†’ Ξ± β†’ Οƒ
f : 
Οƒ: ?m.4711
Οƒ β†’ 
Ξ±: ?m.4718
Ξ± β†’ 
Οƒ: ?m.4711
Οƒ) (
init: Οƒ
init : 
Οƒ: ?m.4711
Οƒ) (
t: Trie Ξ± s
t : 
Trie: Type β†’ Bool β†’ Type
Trie 
Ξ±: ?m.4718
Ξ± 
s: ?m.4730
s) : 
Οƒ: ?m.4711
Οƒ :=
  
Id.run: {Ξ± : Type ?u.4750} β†’ Id Ξ± β†’ Ξ±
Id.run <| 
t: Trie Ξ± s
t.
foldValuesM: {m : Type ?u.4753 β†’ Type ?u.4752} β†’
  {Οƒ : Type ?u.4753} β†’ {Ξ± : Type} β†’ {s : Bool} β†’ [inst : Monad m] β†’ (Οƒ β†’ Ξ± β†’ m Οƒ) β†’ Οƒ β†’ Trie Ξ± s β†’ m Οƒ
foldValuesM (init := 
init: Οƒ
init) 
f: Οƒ β†’ Ξ± β†’ Οƒ
f

/--
The number of values stored in a `Trie`.
-/
partial def 
size: {Ξ± : Type} β†’ {s : Bool} β†’ Trie Ξ± s β†’ Nat
size : 
Trie: Type β†’ Bool β†’ Type
Trie 
Ξ±: ?m.4970
Ξ± 
s: ?m.4975
s β†’ 
Nat: Type
Nat
  | 
Trie.node: {Ξ± : Type} β†’ {simpleReduce : Bool} β†’ Array Ξ± β†’ Array (Key simpleReduce Γ— Trie Ξ± simpleReduce) β†’ Trie Ξ± simpleReduce
Trie.node 
vs: Array Ξ±
vs 
children: Array (Key s Γ— Trie Ξ± s)
children =>
    
children: Array (Key s Γ— Trie Ξ± s)
children.
foldl: {Ξ± : Type ?u.5010} β†’
  {Ξ² : Type ?u.5009} β†’ (Ξ² β†’ Ξ± β†’ Ξ²) β†’ Ξ² β†’ (as : Array Ξ±) β†’ optParam Nat 0 β†’ optParam Nat (Array.size as) β†’ Ξ²
foldl (init := 
vs: Array Ξ±
vs.
size: {Ξ± : Type ?u.5037} β†’ Array Ξ± β†’ Nat
size) fun 
n: ?m.5026
n (_, 
c: Trie Ξ± s
c) => 
n: ?m.5026
n + 
size: {Ξ± : Type} β†’ {s : Bool} β†’ Trie Ξ± s β†’ Nat
size 
c: Trie Ξ± s
c

/--
Merge two `Trie`s. Duplicate values are preserved.
-/
partial def 
mergePreservingDuplicates: {Ξ± : Type} β†’ {s : Bool} β†’ Trie Ξ± s β†’ Trie Ξ± s β†’ Trie Ξ± s
mergePreservingDuplicates : 
Trie: Type β†’ Bool β†’ Type
Trie 
Ξ±: ?m.5597
Ξ± 
s: ?m.5602
s β†’ 
Trie: Type β†’ Bool β†’ Type
Trie 
Ξ±: ?m.5597
Ξ± 
s: ?m.5602
s β†’ 
Trie: Type β†’ Bool β†’ Type
Trie 
Ξ±: ?m.5597
Ξ± 
s: ?m.5602
s
  | 
node: {Ξ± : Type} β†’ {simpleReduce : Bool} β†’ Array Ξ± β†’ Array (Key simpleReduce Γ— Trie Ξ± simpleReduce) β†’ Trie Ξ± simpleReduce
node 
vs₁: Array Ξ±
vs₁ 
cs₁: Array (Key s Γ— Trie Ξ± s)
cs₁, 
node: {Ξ± : Type} β†’ {simpleReduce : Bool} β†’ Array Ξ± β†’ Array (Key simpleReduce Γ— Trie Ξ± simpleReduce) β†’ Trie Ξ± simpleReduce
node 
vsβ‚‚: Array Ξ±
vsβ‚‚ 
csβ‚‚: Array (Key s Γ— Trie Ξ± s)
csβ‚‚ =>
    
node: {Ξ± : Type} β†’ {simpleReduce : Bool} β†’ Array Ξ± β†’ Array (Key simpleReduce Γ— Trie Ξ± simpleReduce) β†’ Trie Ξ± simpleReduce
node (
vs₁: Array Ξ±
vs₁ ++ 
vsβ‚‚: Array Ξ±
vsβ‚‚) (
mergeChildren: Array (Key s Γ— Trie Ξ± s) β†’ Array (Key s Γ— Trie Ξ± s) β†’ Array (Key s Γ— Trie Ξ± s)
mergeChildren 
cs₁: Array (Key s Γ— Trie Ξ± s)
cs₁ 
csβ‚‚: Array (Key s Γ— Trie Ξ± s)
csβ‚‚)
where
  /-- Auxiliary definition for `mergePreservingDuplicates`. -/
  
mergeChildren: {Ξ± : Type} β†’ {s : Bool} β†’ Array (Key s Γ— Trie Ξ± s) β†’ Array (Key s Γ— Trie Ξ± s) β†’ Array (Key s Γ— Trie Ξ± s)
mergeChildren (
cs₁: Array (Key s Γ— Trie Ξ± s)
cs₁ 
csβ‚‚: Array (Key s Γ— Trie Ξ± s)
csβ‚‚ : 
Array: Type ?u.5619 β†’ Type ?u.5619
Array (
Key: Bool β†’ Type
Key 
s: Bool
s Γ— 
Trie: Type β†’ Bool β†’ Type
Trie 
Ξ±: Type
Ξ± 
s: Bool
s)) :
      
Array: Type ?u.5629 β†’ Type ?u.5629
Array (
Key: Bool β†’ Type
Key 
s: Bool
s Γ— 
Trie: Type β†’ Bool β†’ Type
Trie 
Ξ±: Type
Ξ± 
s: Bool
s) :=
    
Array.mergeSortedMergingDuplicates: {Ξ± : Type ?u.5636} β†’ [ord : Ord Ξ±] β†’ Array Ξ± β†’ Array Ξ± β†’ (Ξ± β†’ Ξ± β†’ Ξ±) β†’ Array Ξ±
Array.mergeSortedMergingDuplicates
      (ord := ⟨
compareOn: {Ξ² : Type ?u.5645} β†’ {Ξ± : Sort ?u.5644} β†’ [ord : Ord Ξ²] β†’ (Ξ± β†’ Ξ²) β†’ Ξ± β†’ Ξ± β†’ Ordering
compareOn (Β·.
fst: {Ξ± : Type ?u.5659} β†’ {Ξ² : Type ?u.5658} β†’ Ξ± Γ— Ξ² β†’ Ξ±
fst)⟩) 
cs₁: Array (Key s Γ— Trie Ξ± s)
cs₁ 
csβ‚‚: Array (Key s Γ— Trie Ξ± s)
csβ‚‚
      (fun (
k₁: Key s
k₁, 
t₁: Trie Ξ± s
t₁) (_, 
tβ‚‚: Trie Ξ± s
tβ‚‚) => (
k₁: Key s
k₁, 
mergePreservingDuplicates: {Ξ± : Type} β†’ {s : Bool} β†’ Trie Ξ± s β†’ Trie Ξ± s β†’ Trie Ξ± s
mergePreservingDuplicates 
t₁: Trie Ξ± s
t₁ 
tβ‚‚: Trie Ξ± s
tβ‚‚))

end Trie


/--
Monadically fold over the keys and values stored in a `DiscrTree`.
-/
@[inline]
def 
foldM: {m : Type u_1 β†’ Type u_2} β†’
  {Οƒ : Type u_1} β†’ {s : Bool} β†’ {Ξ± : Type} β†’ [inst : Monad m] β†’ (Οƒ β†’ Array (Key s) β†’ Ξ± β†’ m Οƒ) β†’ Οƒ β†’ DiscrTree Ξ± s β†’ m Οƒ
foldM [
Monad: (Type ?u.6598 β†’ Type ?u.6597) β†’ Type (max(?u.6598+1)?u.6597)
Monad 
m: ?m.6556
m] (
f: Οƒ β†’ Array (Key s) β†’ Ξ± β†’ m Οƒ
f : 
Οƒ: ?m.6566
Οƒ β†’ 
Array: Type ?u.6605 β†’ Type ?u.6605
Array (
Key: Bool β†’ Type
Key 
s: ?m.6579
s) β†’ 
Ξ±: ?m.6594
Ξ± β†’ 
m: ?m.6556
m 
Οƒ: ?m.6566
Οƒ) (
init: Οƒ
init : 
Οƒ: ?m.6566
Οƒ)
    (
t: DiscrTree Ξ± s
t : 
DiscrTree: Type β†’ Bool β†’ Type
DiscrTree 
Ξ±: ?m.6594
Ξ± 
s: ?m.6579
s) : 
m: ?m.6556
m 
Οƒ: ?m.6566
Οƒ :=
  
t: DiscrTree Ξ± s
t.
root: {Ξ± : Type} β†’
  {simpleReduce : Bool} β†’ DiscrTree Ξ± simpleReduce β†’ PersistentHashMap (Key simpleReduce) (Trie Ξ± simpleReduce)
root.
foldlM: {m : Type ?u.6631 β†’ Type ?u.6630} β†’
  [inst : Monad m] β†’
    {Οƒ : Type ?u.6631} β†’
      {Ξ± : Type ?u.6629} β†’
        {Ξ² : Type ?u.6628} β†’ {x : BEq Ξ±} β†’ {x_1 : Hashable Ξ±} β†’ PersistentHashMap Ξ± Ξ² β†’ (Οƒ β†’ Ξ± β†’ Ξ² β†’ m Οƒ) β†’ Οƒ β†’ m Οƒ
foldlM (init := 
init: Οƒ
init) fun 
s: ?m.6682
s 
k: ?m.6685
k 
t: ?m.6688
t => 
t: ?m.6688
t.
foldM: {m : Type ?u.6691 β†’ Type ?u.6690} β†’
  {s : Bool} β†’
    {Οƒ : Type ?u.6691} β†’
      {Ξ± : Type} β†’ [inst : Monad m] β†’ Array (Key s) β†’ (Οƒ β†’ Array (Key s) β†’ Ξ± β†’ m Οƒ) β†’ Οƒ β†’ Trie Ξ± s β†’ m Οƒ
foldM #[
k: ?m.6685
k] (init := 
s: ?m.6682
s) 
f: Οƒ β†’ Array (Key s✝) β†’ Ξ± β†’ m Οƒ
f

/--
Fold over the keys and values stored in a `DiscrTree`
-/
@[inline]
def 
fold: {Οƒ : Sort ?u.6975} β†’ {s : Bool} β†’ {Ξ± : Type} β†’ (Οƒ β†’ Array (Key s) β†’ Ξ± β†’ Οƒ) β†’ Οƒ β†’ DiscrTree Ξ± s β†’ Οƒ
fold (
f: Οƒ β†’ Array (Key s) β†’ Ξ± β†’ Οƒ
f : 
Οƒ: ?m.6954
Οƒ β†’ 
Array: Type ?u.6978 β†’ Type ?u.6978
Array (
Key: Bool β†’ Type
Key 
s: ?m.6962
s) β†’ 
Ξ±: ?m.6972
Ξ± β†’ 
Οƒ: ?m.6954
Οƒ) (
init: Οƒ
init : 
Οƒ: ?m.6954
Οƒ) (
t: DiscrTree Ξ± s
t : 
DiscrTree: Type β†’ Bool β†’ Type
DiscrTree 
Ξ±: ?m.6972
Ξ± 
s: ?m.6962
s) : 
Οƒ: ?m.6954
Οƒ :=
  
Id.run: {Ξ± : Type ?u.6995} β†’ Id Ξ± β†’ Ξ±
Id.run <| 
t: DiscrTree Ξ± s
t.
foldM: {m : Type ?u.6998 β†’ Type ?u.6997} β†’
  {Οƒ : Type ?u.6998} β†’
    {s : Bool} β†’ {Ξ± : Type} β†’ [inst : Monad m] β†’ (Οƒ β†’ Array (Key s) β†’ Ξ± β†’ m Οƒ) β†’ Οƒ β†’ DiscrTree Ξ± s β†’ m Οƒ
foldM (init := 
init: Οƒ
init) fun 
s: ?m.7037
s 
keys: ?m.7040
keys 
a: ?m.7043
a => return 
f: Οƒ β†’ Array (Key s✝) β†’ Ξ± β†’ Οƒ
f 
s: ?m.7037
s 
keys: ?m.7040
keys 
a: ?m.7043
a

/--
Monadically fold over the values stored in a `DiscrTree`.
-/
@[inline]
def 
foldValuesM: {m : Type ?u.7537 β†’ Type ?u.7536} β†’
  {Οƒ : Type ?u.7537} β†’ {Ξ± : Type} β†’ {s : Bool} β†’ [inst : Monad m] β†’ (Οƒ β†’ Ξ± β†’ m Οƒ) β†’ Οƒ β†’ DiscrTree Ξ± s β†’ m Οƒ
foldValuesM [
Monad: (Type ?u.7498 β†’ Type ?u.7497) β†’ Type (max(?u.7498+1)?u.7497)
Monad 
m: ?m.7494
m] (
f: Οƒ β†’ Ξ± β†’ m Οƒ
f : 
Οƒ: ?m.7504
Οƒ β†’ 
Ξ±: ?m.7516
Ξ± β†’ 
m: ?m.7494
m 
Οƒ: ?m.7504
Οƒ) (
init: Οƒ
init : 
Οƒ: ?m.7504
Οƒ) (
t: DiscrTree Ξ± s
t : 
DiscrTree: Type β†’ Bool β†’ Type
DiscrTree 
Ξ±: ?m.7516
Ξ± 
s: ?m.7533
s) :
    
m: ?m.7494
m 
Οƒ: ?m.7504
Οƒ :=
  
t: DiscrTree Ξ± s
t.
root: {Ξ± : Type} β†’
  {simpleReduce : Bool} β†’ DiscrTree Ξ± simpleReduce β†’ PersistentHashMap (Key simpleReduce) (Trie Ξ± simpleReduce)
root.
foldlM: {m : Type ?u.7567 β†’ Type ?u.7566} β†’
  [inst : Monad m] β†’
    {Οƒ : Type ?u.7567} β†’
      {Ξ± : Type ?u.7565} β†’
        {Ξ² : Type ?u.7564} β†’ {x : BEq Ξ±} β†’ {x_1 : Hashable Ξ±} β†’ PersistentHashMap Ξ± Ξ² β†’ (Οƒ β†’ Ξ± β†’ Ξ² β†’ m Οƒ) β†’ Οƒ β†’ m Οƒ
foldlM (init := 
init: Οƒ
init) fun 
s: ?m.7618
s 
_: ?m.7621
_ 
t: ?m.7624
t => 
t: ?m.7624
t.
foldValuesM: {m : Type ?u.7627 β†’ Type ?u.7626} β†’
  {Οƒ : Type ?u.7627} β†’ {Ξ± : Type} β†’ {s : Bool} β†’ [inst : Monad m] β†’ (Οƒ β†’ Ξ± β†’ m Οƒ) β†’ Οƒ β†’ Trie Ξ± s β†’ m Οƒ
foldValuesM (init := 
s: ?m.7618
s) 
f: Οƒ β†’ Ξ± β†’ m Οƒ
f

/--
Fold over the values stored in a `DiscrTree`.
-/
@[inline]
def 
foldValues: {Οƒ : Sort ?u.7870} β†’ {Ξ± : Type} β†’ {s : Bool} β†’ (Οƒ β†’ Ξ± β†’ Οƒ) β†’ Οƒ β†’ DiscrTree Ξ± s β†’ Οƒ
foldValues (
f: Οƒ β†’ Ξ± β†’ Οƒ
f : 
Οƒ: ?m.7848
Οƒ β†’ 
Ξ±: ?m.7855
Ξ± β†’ 
Οƒ: ?m.7848
Οƒ) (
init: Οƒ
init : 
Οƒ: ?m.7848
Οƒ) (
t: DiscrTree Ξ± s
t : 
DiscrTree: Type β†’ Bool β†’ Type
DiscrTree 
Ξ±: ?m.7855
Ξ± 
s: ?m.7867
s) : 
Οƒ: ?m.7848
Οƒ :=
  
Id.run: {Ξ± : Type ?u.7887} β†’ Id Ξ± β†’ Ξ±
Id.run <| 
t: DiscrTree Ξ± s
t.
foldValuesM: {m : Type ?u.7890 β†’ Type ?u.7889} β†’
  {Οƒ : Type ?u.7890} β†’ {Ξ± : Type} β†’ {s : Bool} β†’ [inst : Monad m] β†’ (Οƒ β†’ Ξ± β†’ m Οƒ) β†’ Οƒ β†’ DiscrTree Ξ± s β†’ m Οƒ
foldValuesM (init := 
init: Οƒ
init) 
f: Οƒ β†’ Ξ± β†’ Οƒ
f

/--
Extract the values stored in a `DiscrTree`.
-/
@[inline]
def 
values: {Ξ± : Type} β†’ {s : Bool} β†’ DiscrTree Ξ± s β†’ Array Ξ±
values (
t: DiscrTree Ξ± s
t : 
DiscrTree: Type β†’ Bool β†’ Type
DiscrTree 
Ξ±: ?m.8146
Ξ± 
s: ?m.8150
s) : 
Array: Type ?u.8155 β†’ Type ?u.8155
Array 
Ξ±: ?m.8146
Ξ± :=
  
t: DiscrTree Ξ± s
t.
foldValues: {Οƒ : Type ?u.8160} β†’ {Ξ± : Type} β†’ {s : Bool} β†’ (Οƒ β†’ Ξ± β†’ Οƒ) β†’ Οƒ β†’ DiscrTree Ξ± s β†’ Οƒ
foldValues (init := 
#[]: Array ?m.8190
#[]) fun 
as: ?m.8174
as 
a: ?m.8177
a => 
as: ?m.8174
as.
push: {Ξ± : Type ?u.8179} β†’ Array Ξ± β†’ Ξ± β†’ Array Ξ±
push 
a: ?m.8177
a

/--
Extract the keys and values stored in a `DiscrTree`.
-/
@[inline]
def 
toArray: {Ξ± : Type} β†’ {s : Bool} β†’ DiscrTree Ξ± s β†’ Array (Array (Key s) Γ— Ξ±)
toArray (
t: DiscrTree Ξ± s
t : 
DiscrTree: Type β†’ Bool β†’ Type
DiscrTree 
Ξ±: ?m.8350
Ξ± 
s: ?m.8354
s) : 
Array: Type ?u.8359 β†’ Type ?u.8359
Array (
Array: Type ?u.8362 β†’ Type ?u.8362
Array (
Key: Bool β†’ Type
Key 
s: ?m.8354
s) Γ— 
Ξ±: ?m.8350
Ξ±) :=
  
t: DiscrTree Ξ± s
t.
fold: {Οƒ : Type ?u.8367} β†’ {s : Bool} β†’ {Ξ± : Type} β†’ (Οƒ β†’ Array (Key s) β†’ Ξ± β†’ Οƒ) β†’ Οƒ β†’ DiscrTree Ξ± s β†’ Οƒ
fold (init := 
#[]: Array ?m.8409
#[]) fun 
as: ?m.8381
as 
keys: ?m.8384
keys 
a: ?m.8387
a => 
as: ?m.8381
as.
push: {Ξ± : Type ?u.8389} β†’ Array Ξ± β†’ Ξ± β†’ Array Ξ±
push (
keys: ?m.8384
keys, 
a: ?m.8387
a)

/--
Get the number of values stored in a `DiscrTree`. O(n) in the size of the tree.
-/
@[inline]
def 
size: {Ξ± : Type} β†’ {s : Bool} β†’ DiscrTree Ξ± s β†’ Nat
size (
t: DiscrTree Ξ± s
t : 
DiscrTree: Type β†’ Bool β†’ Type
DiscrTree 
Ξ±: ?m.8652
Ξ± 
s: ?m.8656
s) : 
Nat: Type
Nat :=
  
t: DiscrTree Ξ± s
t.
root: {Ξ± : Type} β†’
  {simpleReduce : Bool} β†’ DiscrTree Ξ± simpleReduce β†’ PersistentHashMap (Key simpleReduce) (Trie Ξ± simpleReduce)
root.
foldl: {Οƒ : Type ?u.8671} β†’
  {Ξ± : Type ?u.8670} β†’
    {Ξ² : Type ?u.8669} β†’ {x : BEq Ξ±} β†’ {x_1 : Hashable Ξ±} β†’ PersistentHashMap Ξ± Ξ² β†’ (Οƒ β†’ Ξ± β†’ Ξ² β†’ Οƒ) β†’ Οƒ β†’ Οƒ
foldl (init := 
0: ?m.8753
0) fun 
n: ?m.8697
n 
_: ?m.8700
_ 
t: ?m.8703
t => 
n: ?m.8697
n + 
t: ?m.8703
t.
size: {Ξ± : Type} β†’ {s : Bool} β†’ Trie Ξ± s β†’ Nat
size

/--
Merge two `DiscrTree`s. Duplicate values are preserved.
-/
@[inline]
def 
mergePreservingDuplicates: {Ξ± : Type} β†’ {s : Bool} β†’ DiscrTree Ξ± s β†’ DiscrTree Ξ± s β†’ DiscrTree Ξ± s
mergePreservingDuplicates (
t: DiscrTree Ξ± s
t 
u: DiscrTree Ξ± s
u : 
DiscrTree: Type β†’ Bool β†’ Type
DiscrTree 
Ξ±: ?m.8896
Ξ± 
s: ?m.8900
s) : 
DiscrTree: Type β†’ Bool β†’ Type
DiscrTree 
Ξ±: ?m.8896
Ξ± 
s: ?m.8900
s :=
  ⟨
t: DiscrTree Ξ± s
t.
root: {Ξ± : Type} β†’
  {simpleReduce : Bool} β†’ DiscrTree Ξ± simpleReduce β†’ PersistentHashMap (Key simpleReduce) (Trie Ξ± simpleReduce)
root.
mergeWith: {Ξ± : Type ?u.8922} β†’
  [inst : BEq Ξ±] β†’
    [inst_1 : Hashable Ξ±] β†’
      {Ξ² : Type ?u.8921} β†’ PersistentHashMap Ξ± Ξ² β†’ PersistentHashMap Ξ± Ξ² β†’ (Ξ± β†’ Ξ² β†’ Ξ² β†’ Ξ²) β†’ PersistentHashMap Ξ± Ξ²
mergeWith 
u: DiscrTree Ξ± s
u.
root: {Ξ± : Type} β†’
  {simpleReduce : Bool} β†’ DiscrTree Ξ± simpleReduce β†’ PersistentHashMap (Key simpleReduce) (Trie Ξ± simpleReduce)
root fun 
_: ?m.8951
_ 
trie₁: ?m.8954
trie₁ 
trieβ‚‚: ?m.8957
trieβ‚‚ =>
    
trie₁: ?m.8954
trie₁.
mergePreservingDuplicates: {Ξ± : Type} β†’ {s : Bool} β†’ Trie Ξ± s β†’ Trie Ξ± s β†’ Trie Ξ± s
mergePreservingDuplicates 
trieβ‚‚: ?m.8957
trieβ‚‚βŸ©