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

chore: move to new frontend

Browse source
This commit is contained in:
Leonardo de Moura 2020-10-20 16:13:07 -07:00
parent 6b132a23e9
commit 93f7b1d7bc
6 changed files with 81 additions and 75 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Lean/Data/Json/Basic.lean
View file

@ -5,6 +5,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: Gabriel Ebner, Marc Huisinga
-/
import Std.Data.RBTree
namespace Std end Std -- Hack for old frontend
namespace Lean
-- mantissa * 10^-exponent

2
src/Lean/Level.lean
View file

@ -10,6 +10,8 @@ import Std.Data.PersistentHashSet
import Lean.Data.Name
import Lean.Data.Format
namespace Std end Std -- Hack for old frontend
def Nat.imax (n m : Nat) : Nat :=
if m = 0 then 0 else Nat.max n m

44
src/Std/Data/HashSet.lean
View file

@ -1,3 +1,4 @@
#lang lean4
/-
Copyright (c) 2019 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
@ -18,16 +19,16 @@ structure HashSetImp (α : Type u) :=
(buckets : HashSetBucket α)
def mkHashSetImp {α : Type u} (nbuckets := 8) : HashSetImp α :=
let n := if nbuckets = 0 then 8 else nbuckets;
let n := if nbuckets = 0 then 8 else nbuckets
{ size := 0,
buckets :=
⟨ mkArray n [],
have p₁ : (mkArray n ([] : List α)).size = n from Array.szMkArrayEq _ _;
have p₂ : n = (if nbuckets = 0 then 8 else nbuckets) from rfl;
have p₁ : (mkArray n ([] : List α)).size = n from Array.szMkArrayEq _ _
have p₂ : n = (if nbuckets = 0 then 8 else nbuckets) from rfl
have p₃ : (if nbuckets = 0 then 8 else nbuckets) > 0 from
match nbuckets with
| 0 => Nat.zeroLtSucc _
| (Nat.succ x) => Nat.zeroLtSucc _;
| (Nat.succ x) => Nat.zeroLtSucc _
transRelRight Greater (Eq.trans p₁ p₂) p₃ ⟩ }
namespace HashSetImp
@ -37,7 +38,7 @@ def mkIdx {n : Nat} (h : n > 0) (u : USize) : { u : USize // u.toNat < n } :=
⟨u %ₙ n, USize.modnLt _ h⟩
@[inline] def reinsertAux (hashFn : α → USize) (data : HashSetBucket α) (a : α) : HashSetBucket α :=
let ⟨i, h⟩ := mkIdx data.property (hashFn a);
let ⟨i, h⟩ := mkIdx data.property (hashFn a)
data.update i (a :: data.val.uget i h) h
@[inline] def foldBucketsM {δ : Type w} {m : Type w → Type w} [Monad m] (data : HashSetBucket α) (d : δ) (f : δ → α → m δ) : m δ :=
@ -55,45 +56,46 @@ foldBuckets m.buckets d f
def find? [HasBeq α] [Hashable α] (m : HashSetImp α) (a : α) : Option α :=
match m with
| ⟨_, buckets⟩ =>
let ⟨i, h⟩ := mkIdx buckets.property (hash a);
let ⟨i, h⟩ := mkIdx buckets.property (hash a)
(buckets.val.uget i h).find? (fun a' => a == a')
def contains [HasBeq α] [Hashable α] (m : HashSetImp α) (a : α) : Bool :=
match m with
| ⟨_, buckets⟩ =>
let ⟨i, h⟩ := mkIdx buckets.property (hash a);
let ⟨i, h⟩ := mkIdx buckets.property (hash a)
(buckets.val.uget i h).contains a
-- TODO: remove `partial` by using well-founded recursion
partial def moveEntries [Hashable α] : Nat → Array (List α) → HashSetBucket α → HashSetBucket α
| i, source, target =>
if h : i < source.size then
let idx : Fin source.size := ⟨i, h⟩;
let es : List α := source.get idx;
let idx : Fin source.size := ⟨i, h⟩
let es : List α := source.get idx
-- We remove `es` from `source` to make sure we can reuse its memory cells when performing es.foldl
let source := source.set idx [];
let target := es.foldl (reinsertAux hash) target;
let source := source.set idx []
let target := es.foldl (reinsertAux hash) target
moveEntries (i+1) source target
else target
def expand [Hashable α] (size : Nat) (buckets : HashSetBucket α) : HashSetImp α :=
let nbuckets := buckets.val.size * 2;
have aux₁ : nbuckets > 0 from Nat.mulPos buckets.property (Nat.zeroLtBit0 Nat.oneNeZero);
have aux₂ : (mkArray nbuckets ([] : List α)).size = nbuckets from Array.szMkArrayEq _ _;
let new_buckets : HashSetBucket α := ⟨mkArray nbuckets [], aux₂.symm ▸ aux₁⟩;
let nbuckets := buckets.val.size * 2
have nbuckets > 0 from Nat.mulPos buckets.property (Nat.zeroLtBit0 Nat.oneNeZero)
have (mkArray nbuckets ([] : List α)).size = nbuckets from Array.szMkArrayEq _ _
have Array.size (mkArray nbuckets List.nil) > 0 by rw this; assumption
let new_buckets : HashSetBucket α := ⟨mkArray nbuckets [], this⟩;
{ size := size,
buckets := moveEntries 0 buckets.val new_buckets }
def insert [HasBeq α] [Hashable α] (m : HashSetImp α) (a : α) : HashSetImp α :=
match m with
| ⟨size, buckets⟩ =>
let ⟨i, h⟩ := mkIdx buckets.property (hash a);
let bkt := buckets.val.uget i h;
let ⟨i, h⟩ := mkIdx buckets.property (hash a)
let bkt := buckets.val.uget i h
if bkt.contains a
then ⟨size, buckets.update i (bkt.replace a a) h⟩
else
let size' := size + 1;
let buckets' := buckets.update i (a :: bkt) h;
let size' := size + 1
let buckets' := buckets.update i (a :: bkt) h
if size' ≤ buckets.val.size
then { size := size', buckets := buckets' }
else expand size' buckets'
@ -101,8 +103,8 @@ match m with
def erase [HasBeq α] [Hashable α] (m : HashSetImp α) (a : α) : HashSetImp α :=
match m with
| ⟨ size, buckets ⟩ =>
let ⟨i, h⟩ := mkIdx buckets.property (hash a);
let bkt := buckets.val.uget i h;
let ⟨i, h⟩ := mkIdx buckets.property (hash a)
let bkt := buckets.val.uget i h
if bkt.contains a then ⟨size - 1, buckets.update i (bkt.erase a) h⟩
else m

106
src/Std/Data/PersistentHashMap.lean
View file

@ -1,3 +1,4 @@
#lang lean4
/-
Copyright (c) 2019 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
@ -9,15 +10,15 @@ universes u v w w'
namespace PersistentHashMap
inductive Entry (α : Type u) (β : Type v) (σ : Type w)
| entry (key : α) (val : β) : Entry
| ref (node : σ) : Entry
| null : Entry
| entry (key : α) (val : β) : Entry α β σ
| ref (node : σ) : Entry α β σ
| null : Entry α β σ
instance Entry.inhabited {α β σ} : Inhabited (Entry α β σ) := ⟨Entry.null⟩
inductive Node (α : Type u) (β : Type v) : Type (max u v)
| entries (es : Array (Entry α β Node)) : Node
| collision (ks : Array α) (vs : Array β) (h : ks.size = vs.size) : Node
| entries (es : Array (Entry α β (Node α β))) : Node α β
| collision (ks : Array α) (vs : Array β) (h : ks.size = vs.size) : Node α β
instance Node.inhabited {α β} : Inhabited (Node α β) := ⟨Node.entries #[]⟩
@ -66,14 +67,14 @@ abbrev EntriesNode (α β) := { n : Node α β // IsEntriesNode n }
private theorem setSizeEq {ks : Array α} {vs : Array β} (h : ks.size = vs.size) (i : Fin ks.size) (j : Fin vs.size) (k : α) (v : β)
: (ks.set i k).size = (vs.set j v).size :=
have h₁ : (ks.set i k).size = ks.size from Array.szFSetEq _ _ _;
have h₂ : (vs.set j v).size = vs.size from Array.szFSetEq _ _ _;
have h₁ : (ks.set i k).size = ks.size by apply Array.szFSetEq
have h₂ : (vs.set j v).size = vs.size by apply Array.szFSetEq
(h₁.trans h).trans h₂.symm
private theorem pushSizeEq {ks : Array α} {vs : Array β} (h : ks.size = vs.size) (k : α) (v : β) : (ks.push k).size = (vs.push v).size :=
have h₁ : (ks.push k).size = ks.size + 1 from Array.szPushEq _ _;
have h₂ : (vs.push v).size = vs.size + 1 from Array.szPushEq _ _;
have h₃ : ks.size + 1 = vs.size + 1 from h ▸ rfl;
have h₁ : (ks.push k).size = ks.size + 1 by apply Array.szPushEq
have h₂ : (vs.push v).size = vs.size + 1 by apply Array.szPushEq
have h₃ : ks.size + 1 = vs.size + 1 by rw h; exact rfl
(h₁.trans h₃).trans h₂.symm
partial def insertAtCollisionNodeAux [HasBeq α] : CollisionNode α β → Nat → α → β → CollisionNode α β
@ -82,7 +83,7 @@ partial def insertAtCollisionNodeAux [HasBeq α] : CollisionNode α β → Nat
let idx : Fin keys.size := ⟨i, h⟩;
let k' := keys.get idx;
if k == k' then
let j : Fin vals.size := ⟨i, heq ▸ h⟩;
let j : Fin vals.size := ⟨i, by rw [←heq]; assumption⟩
⟨Node.collision (keys.set idx k) (vals.set j v) (setSizeEq heq idx j k v), IsCollisionNode.mk _ _ _⟩
else insertAtCollisionNodeAux n (i+1) k v
else
@ -97,30 +98,28 @@ def getCollisionNodeSize : CollisionNode α β → Nat
| ⟨Node.entries _, h⟩ => False.elim (nomatch h)
def mkCollisionNode (k₁ : α) (v₁ : β) (k₂ : α) (v₂ : β) : Node α β :=
let ks : Array α := Array.mkEmpty maxCollisions;
let ks := (ks.push k₁).push k₂;
let vs : Array β := Array.mkEmpty maxCollisions;
let vs := (vs.push v₁).push v₂;
let ks : Array α := Array.mkEmpty maxCollisions
let ks := (ks.push k₁).push k₂
let vs : Array β := Array.mkEmpty maxCollisions
let vs := (vs.push v₁).push v₂
Node.collision ks vs rfl
partial def insertAux [HasBeq α] [Hashable α] : Node α β → USize → USize → α → β → Node α β
| Node.collision keys vals heq, _, depth, k, v =>
let newNode := insertAtCollisionNode ⟨Node.collision keys vals heq, IsCollisionNode.mk _ _ _⟩ k v;
let newNode := insertAtCollisionNode ⟨Node.collision keys vals heq, IsCollisionNode.mk _ _ _⟩ k v
if depth >= maxDepth || getCollisionNodeSize newNode < maxCollisions then newNode.val
else match newNode with
| ⟨Node.entries _, h⟩ => False.elim (nomatch h)
| ⟨Node.collision keys vals heq, _⟩ =>
let entries : Node α β := mkEmptyEntries;
keys.iterate entries $ fun i k entries =>
let v := vals.get ⟨i.val, heq ▸ i.isLt⟩;
let h := hash k;
-- dbgTrace ("toCollision " ++ toString i ++ ", h: " ++ toString h ++ ", depth: " ++ toString depth ++ ", h': " ++
-- toString (div2Shift h (shift * (depth - 1)))) $ fun _ =>
let h := div2Shift h (shift * (depth - 1));
let entries : Node α β := mkEmptyEntries
keys.iterate entries fun i k entries =>
let v := vals.get ⟨i.val, by rw [←heq]; exact i.isLt⟩
let h := hash k
let h := div2Shift h (shift * (depth - 1))
insertAux entries h depth k v
| Node.entries entries, h, depth, k, v =>
let j := (mod2Shift h shift).toNat;
Node.entries $ entries.modify j $ fun entry =>
let j := (mod2Shift h shift).toNat
Node.entries $ entries.modify j fun entry =>
match entry with
| Entry.null => Entry.entry k v
| Entry.ref node => Entry.ref $ insertAux node (div2Shift h shift) (depth+1) k v
@ -134,14 +133,14 @@ def insert [HasBeq α] [Hashable α] : PersistentHashMap α β → α → β →
partial def findAtAux [HasBeq α] (keys : Array α) (vals : Array β) (heq : keys.size = vals.size) : Nat → α → Option β
| i, k =>
if h : i < keys.size then
let k' := keys.get ⟨i, h⟩;
if k == k' then some (vals.get ⟨i, heq ▸ h⟩)
else findAtAux (i+1) k
let k' := keys.get ⟨i, h⟩
if k == k' then some (vals.get ⟨i, by rw [←heq]; assumption⟩)
else findAtAux keys vals heq (i+1) k
else none
partial def findAux [HasBeq α] : Node α β → USize → α → Option β
| Node.entries entries, h, k =>
let j := (mod2Shift h shift).toNat;
let j := (mod2Shift h shift).toNat
match entries.get! j with
| Entry.null => none
| Entry.ref node => findAux node (div2Shift h shift) k
@ -165,14 +164,14 @@ match m.find? a with
partial def findEntryAtAux [HasBeq α] (keys : Array α) (vals : Array β) (heq : keys.size = vals.size) : Nat → α → Option (α × β)
| i, k =>
if h : i < keys.size then
let k' := keys.get ⟨i, h⟩;
if k == k' then some (k', vals.get ⟨i, heq ▸ h⟩)
else findEntryAtAux (i+1) k
let k' := keys.get ⟨i, h⟩
if k == k' then some (k', vals.get ⟨i, by rw [←heq]; assumption⟩)
else findEntryAtAux keys vals heq (i+1) k
else none
partial def findEntryAux [HasBeq α] : Node α β → USize → α → Option (α × β)
| Node.entries entries, h, k =>
let j := (mod2Shift h shift).toNat;
let j := (mod2Shift h shift).toNat
match entries.get! j with
| Entry.null => none
| Entry.ref node => findEntryAux node (div2Shift h shift) k
@ -185,14 +184,14 @@ def findEntry? [HasBeq α] [Hashable α] : PersistentHashMap α β → α → Op
partial def containsAtAux [HasBeq α] (keys : Array α) (vals : Array β) (heq : keys.size = vals.size) : Nat → α → Bool
| i, k =>
if h : i < keys.size then
let k' := keys.get ⟨i, h⟩;
let k' := keys.get ⟨i, h⟩
if k == k' then true
else containsAtAux (i+1) k
else containsAtAux keys vals heq (i+1) k
else false
partial def containsAux [HasBeq α] : Node α β → USize → α → Bool
| Node.entries entries, h, k =>
let j := (mod2Shift h shift).toNat;
let j := (mod2Shift h shift).toNat
match entries.get! j with
| Entry.null => false
| Entry.ref node => containsAux node (div2Shift h shift) k
@ -206,11 +205,11 @@ partial def isUnaryEntries (a : Array (Entry α β (Node α β))) : Nat → Opti
| i, acc =>
if h : i < a.size then
match a.get ⟨i, h⟩ with
| Entry.null => isUnaryEntries (i+1) acc
| Entry.null => isUnaryEntries a (i+1) acc
| Entry.ref _ => none
| Entry.entry k v =>
match acc with
| none => isUnaryEntries (i+1) (some (k, v))
| none => isUnaryEntries a (i+1) (some (k, v))
| some _ => none
else acc
@ -218,8 +217,8 @@ def isUnaryNode : Node α β → Option (α × β)
| Node.entries entries => isUnaryEntries entries 0 none
| Node.collision keys vals heq =>
if h : 1 = keys.size then
have 0 < keys.size from h ▸ (Nat.zeroLtSucc _);
some (keys.get ⟨0, this⟩, vals.get ⟨0, heq ▸ this⟩)
have 0 < keys.size by rw [←h]; exact decide!
some (keys.get ⟨0, this⟩, vals.get ⟨0, by rw [←heq]; assumption⟩)
else
none
@ -227,21 +226,21 @@ partial def eraseAux [HasBeq α] : Node α β → USize → α → Node α β ×
| n@(Node.collision keys vals heq), _, k =>
match keys.indexOf? k with
| some idx =>
let ⟨keys', keq⟩ := keys.eraseIdx' idx;
let ⟨vals', veq⟩ := vals.eraseIdx' (Eq.rec idx heq);
have keys.size - 1 = vals.size - 1 from heq ▸ rfl;
let ⟨keys', keq⟩ := keys.eraseIdx' idx
let ⟨vals', veq⟩ := vals.eraseIdx' (Eq.ndrec idx heq)
have keys.size - 1 = vals.size - 1 by rw [heq]; exact rfl
(Node.collision keys' vals' (keq.trans (this.trans veq.symm)), true)
| none => (n, false)
| n@(Node.entries entries), h, k =>
let j := (mod2Shift h shift).toNat;
let entry := entries.get! j;
let j := (mod2Shift h shift).toNat
let entry := entries.get! j
match entry with
| Entry.null => (n, false)
| Entry.entry k' v =>
if k == k' then (Node.entries (entries.set! j Entry.null), true) else (n, false)
| Entry.ref node =>
let entries := entries.set! j Entry.null;
let (newNode, deleted) := eraseAux node (div2Shift h shift) k;
let entries := entries.set! j Entry.null
let (newNode, deleted) := eraseAux node (div2Shift h shift) k
if !deleted then (n, false)
else match isUnaryNode newNode with
| none => (Node.entries (entries.set! j (Entry.ref newNode)), true)
@ -249,8 +248,8 @@ partial def eraseAux [HasBeq α] : Node α β → USize → α → Node α β ×
def erase [HasBeq α] [Hashable α] : PersistentHashMap α β → α → PersistentHashMap α β
| { root := n, size := sz }, k =>
let h := hash k;
let (n, del) := eraseAux n h k;
let h := hash k
let (n, del) := eraseAux n h k
{ root := n, size := if del then sz - 1 else sz }
section
@ -258,12 +257,12 @@ variables {m : Type w → Type w'} [Monad m]
variables {σ : Type w}
@[specialize] partial def foldlMAux (f : σ → α → β → m σ) : Node α β → σ → m σ
| Node.collision keys vals heq, acc => keys.iterateM acc $ fun i k acc => f acc k (vals.get ⟨i.val, heq ▸ i.isLt⟩)
| Node.collision keys vals heq, acc => keys.iterateM acc fun i k acc => f acc k (vals.get ⟨i.val, by rw [←heq]; exact i.isLt⟩)
| Node.entries entries, acc => entries.foldlM (fun acc entry =>
match entry with
| Entry.null => pure acc
| Entry.entry k v => f acc k v
| Entry.ref node => foldlMAux node acc)
| Entry.ref node => foldlMAux f node acc)
acc
@[specialize] def foldlM [HasBeq α] [Hashable α] (map : PersistentHashMap α β) (f : σ → α → β → m σ) (acc : σ) : m σ :=
@ -295,7 +294,7 @@ partial def collectStats : Node α β → Stats → Nat → Stats
let stats :=
{ stats with
numNodes := stats.numNodes + 1,
maxDepth := Nat.max stats.maxDepth depth };
maxDepth := Nat.max stats.maxDepth depth }
entries.foldl (fun stats entry =>
match entry with
| Entry.null => { stats with numNull := stats.numNull + 1 }
@ -307,8 +306,7 @@ def stats [HasBeq α] [Hashable α] (m : PersistentHashMap α β) : Stats :=
collectStats m.root {} 1
def Stats.toString (s : Stats) : String :=
"{ nodes := " ++ toString s.numNodes ++ ", null := " ++ toString s.numNull ++
", collisions := " ++ toString s.numCollisions ++ ", depth := " ++ toString s.maxDepth ++ "}"
s!"\{ nodes := {s.numNodes}, null := {s.numNull}, collisions := {s.numCollisions}, depth := {s.maxDepth}}"
instance : HasToString Stats := ⟨Stats.toString⟩

1
src/Std/Data/PersistentHashSet.lean
View file

@ -1,3 +1,4 @@
#lang lean4
/-
Copyright (c) 2019 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.

1
src/Std/Data/RBTree.lean
View file

@ -1,3 +1,4 @@
#lang lean4
/-
Copyright (c) 2017 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.