From ab487ea4ac4a2e3aa3d6faeb020c726e3387da4a Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 27 Jun 2019 17:12:03 -0700 Subject: [PATCH] feat(frontends/lean): allow `;` instead of `in` in let-decls --- library/init/core.lean | 12 +- library/init/data/array/basic.lean | 54 +-- library/init/data/array/binsearch.lean | 4 +- library/init/data/array/qsort.lean | 22 +- library/init/data/char/basic.lean | 4 +- library/init/data/hashmap/basic.lean | 32 +- library/init/data/nat/bitwise.lean | 10 +- library/init/data/persistentarray/basic.lean | 22 +- library/init/data/random.lean | 56 +-- library/init/data/rbmap/basic.lean | 2 +- library/init/data/repr.lean | 10 +- library/init/data/string/basic.lean | 67 +-- library/init/lean/attributes.lean | 18 +- .../init/lean/compiler/closedtermcache.lean | 2 +- library/init/lean/compiler/constfolding.lean | 8 +- library/init/lean/compiler/exportattr.lean | 2 +- library/init/lean/compiler/externattr.lean | 16 +- library/init/lean/compiler/ir/basic.lean | 12 +- library/init/lean/compiler/ir/borrow.lean | 16 +- library/init/lean/compiler/ir/boxing.lean | 26 +- library/init/lean/compiler/ir/compilerm.lean | 6 +- library/init/lean/compiler/ir/elimdead.lean | 20 +- library/init/lean/compiler/ir/emitcpp.lean | 10 +- library/init/lean/compiler/ir/emitutil.lean | 2 +- .../lean/compiler/ir/expandresetreuse.lean | 50 +-- library/init/lean/compiler/ir/format.lean | 6 +- library/init/lean/compiler/ir/livevars.lean | 6 +- library/init/lean/compiler/ir/pushproj.lean | 26 +- library/init/lean/compiler/ir/rc.lean | 92 ++--- library/init/lean/compiler/ir/resetreuse.lean | 12 +- library/init/lean/compiler/ir/simpcase.lean | 22 +- library/init/lean/compiler/namemangling.lean | 28 +- library/init/lean/compiler/util.lean | 2 +- library/init/lean/environment.lean | 18 +- library/init/lean/format.lean | 12 +- library/init/lean/level.lean | 4 +- library/init/lean/modifiers.lean | 8 +- library/init/lean/name.lean | 2 +- library/init/lean/parser/parser.lean | 390 +++++++++--------- library/init/lean/parser/trie.lean | 20 +- library/init/lean/position.lean | 10 +- library/init/lean/syntax.lean | 40 +- src/frontends/lean/builtin_exprs.cpp | 7 +- 43 files changed, 594 insertions(+), 594 deletions(-) diff --git a/library/init/core.lean b/library/init/core.lean index 9d078422b9..6506251a5a 100644 --- a/library/init/core.lean +++ b/library/init/core.lean @@ -1691,7 +1691,7 @@ axiom choice {α : Sort u} : Nonempty α → α noncomputable def indefiniteDescription {α : Sort u} (p : α → Prop) (h : Exists (λ x, p x)) : {x // p x} := -choice $ let ⟨x, px⟩ := h in ⟨⟨x, px⟩⟩ +choice $ let ⟨x, px⟩ := h; ⟨⟨x, px⟩⟩ noncomputable def choose {α : Sort u} {p : α → Prop} (h : Exists (λ x, p x)) : α := (indefiniteDescription p h).val @@ -1701,12 +1701,12 @@ theorem chooseSpec {α : Sort u} {p : α → Prop} (h : Exists (λ x, p x)) : p /- Diaconescu's theorem: excluded middle from choice, Function extensionality and propositional extensionality. -/ theorem em (p : Prop) : p ∨ ¬p := -let U (x : Prop) : Prop := x = True ∨ p in -let V (x : Prop) : Prop := x = False ∨ p in +let U (x : Prop) : Prop := x = True ∨ p; +let V (x : Prop) : Prop := x = False ∨ p; have exU : Exists (λ x, U x), from ⟨True, Or.inl rfl⟩, have exV : Exists (λ x, V x), from ⟨False, Or.inl rfl⟩, -let u : Prop := choose exU in -let v : Prop := choose exV in +let u : Prop := choose exU; +let v : Prop := choose exV; have uDef : U u, from chooseSpec exU, have vDef : V v, from chooseSpec exV, have notUvOrP : u ≠ v ∨ p, from @@ -1767,7 +1767,7 @@ noncomputable def strongIndefiniteDescription {α : Sort u} (p : α → Prop) @dite (Exists (λ x : α, p x)) (propDecidable _) _ (λ hp : Exists (λ x : α, p x), show {x : α // Exists (λ y : α, p y) → p x}, from - let xp := indefiniteDescription _ hp in + let xp := indefiniteDescription _ hp; ⟨xp.val, λ h', xp.property⟩) (λ hp, ⟨choice h, λ h, absurd h hp⟩) diff --git a/library/init/data/array/basic.lean b/library/init/data/array/basic.lean index 374ed821ff..096ba56eae 100644 --- a/library/init/data/array/basic.lean +++ b/library/init/data/array/basic.lean @@ -106,9 +106,9 @@ if h : i < a.size then a.fset ⟨i, h⟩ v else a @[extern cpp inline "lean::array_fswap(#2, #3, #4)"] def fswap (a : Array α) (i j : @& Fin a.size) : Array α := -let v₁ := a.fget i in -let v₂ := a.fget j in -let a := a.fset i v₂ in +let v₁ := a.fget i; +let v₂ := a.fget j; +let a := a.fset i v₂; a.fset j v₁ @[extern cpp inline "lean::array_swap(#2, #3, #4)"] @@ -119,8 +119,8 @@ else a else a @[inline] def fswapAt {α : Type} (a : Array α) (i : Fin a.size) (v : α) : α × Array α := -let e := a.fget i in -let a := a.fset i v in +let e := a.fget i; +let a := a.fset i v; (e, a) @[inline] def swapAt {α : Type} (a : Array α) (i : Nat) (v : α) : α × Array α := @@ -142,7 +142,7 @@ variables {m : Type v → Type v} [Monad m] @[specialize] partial def miterateAux (a : Array α) (f : Π i : Fin a.size, α → β → m β) : Nat → β → m β | i b := if h : i < a.size then - let idx : Fin a.size := ⟨i, h⟩ in + let idx : Fin a.size := ⟨i, h⟩; f idx (a.fget idx) b >>= miterateAux (i+1) else pure b @@ -159,9 +159,9 @@ miterateAux a (λ _ b a, f a b) ini b @[specialize] partial def miterate₂Aux (a₁ : Array α) (a₂ : Array σ) (f : Π i : Fin a₁.size, α → σ → β → m β) : Nat → β → m β | i b := if h₁ : i < a₁.size then - let idx₁ : Fin a₁.size := ⟨i, h₁⟩ in + let idx₁ : Fin a₁.size := ⟨i, h₁⟩; if h₂ : i < a₂.size then - let idx₂ : Fin a₂.size := ⟨i, h₂⟩ in + let idx₂ : Fin a₂.size := ⟨i, h₂⟩; f idx₁ (a₁.fget idx₁) (a₂.fget idx₂) b >>= miterate₂Aux (i+1) else pure b else pure b @@ -176,7 +176,7 @@ miterate₂ a₁ a₂ b (λ _ a₁ a₂ b, f b a₁ a₂) @[specialize] partial def mfindAux (a : Array α) (f : α → m (Option β)) : Nat → m (Option β) | i := if h : i < a.size then - let idx : Fin a.size := ⟨i, h⟩ in + let idx : Fin a.size := ⟨i, h⟩; do r ← f (a.fget idx), match r with | some v := pure r @@ -215,7 +215,7 @@ variables {m : Type → Type v} [Monad m] @[specialize] partial def anyMAux (a : Array α) (p : α → m Bool) : Nat → m Bool | i := if h : i < a.size then - let idx : Fin a.size := ⟨i, h⟩ in + let idx : Fin a.size := ⟨i, h⟩; do b ← p (a.fget idx), match b with | true := pure true @@ -238,7 +238,7 @@ Id.run $ anyM a p @[specialize] private def revIterateAux (a : Array α) (f : Π i : Fin a.size, α → β → β) : Π (i : Nat), i ≤ a.size → β → β | 0 h b := b | (j+1) h b := - let i : Fin a.size := ⟨j, h⟩ in + let i : Fin a.size := ⟨j, h⟩; revIterateAux j (Nat.leOfLt h) (f i (a.fget i) b) @[inline] def revIterate (a : Array α) (b : β) (f : Π i : Fin a.size, α → β → β) : β := @@ -263,9 +263,9 @@ variables {m : Type v → Type v} [Monad m] @[specialize] unsafe partial def ummapAux (f : Nat → α → m β) : Nat → Array α → m (Array β) | i a := if h : i < a.size then - let idx : Fin a.size := ⟨i, h⟩ in - let v : α := a.fget idx in - let a := a.fset idx (@unsafeCast _ _ ⟨v⟩ ()) in + let idx : Fin a.size := ⟨i, h⟩; + let v : α := a.fget idx; + let a := a.fset idx (@unsafeCast _ _ ⟨v⟩ ()); do newV ← f i v, ummapAux (i+1) (a.fset idx (@unsafeCast _ _ ⟨v⟩ newV)) else pure (unsafeCast a) @@ -285,10 +285,10 @@ end @[inline] def modify [Inhabited α] (a : Array α) (i : Nat) (f : α → α) : Array α := if h : i < a.size then - let idx : Fin a.size := ⟨i, h⟩ in - let v := a.fget idx in - let a := a.fset idx (default α) in - let v := f v in + let idx : Fin a.size := ⟨i, h⟩; + let v := a.fget idx; + let a := a.fset idx (default α); + let v := f v; a.fset idx v else a @@ -306,8 +306,8 @@ variables {m : Type u → Type u} [Monad m] partial def mforAux {α : Type w} {β : Type u} (f : α → m β) (a : Array α) : Nat → m PUnit | i := if h : i < a.size then - let idx : Fin a.size := ⟨i, h⟩ in - let v : α := a.fget idx in + let idx : Fin a.size := ⟨i, h⟩; + let v : α := a.fget idx; f v *> mforAux (i+1) else pure ⟨⟩ @@ -321,12 +321,12 @@ end partial def extractAux (a : Array α) : Nat → Π (e : Nat), e ≤ a.size → Array α → Array α | i e hle r := if hlt : i < e then - let idx : Fin a.size := ⟨i, Nat.ltOfLtOfLe hlt hle⟩ in + let idx : Fin a.size := ⟨i, Nat.ltOfLtOfLe hlt hle⟩; extractAux (i+1) e hle (r.push (a.fget idx)) else r def extract (a : Array α) (b e : Nat) : Array α := -let r : Array α := mkEmpty (e - b) in +let r : Array α := mkEmpty (e - b); if h : e ≤ a.size then extractAux a b e h r else r @@ -339,8 +339,8 @@ instance : HasAppend (Array α) := ⟨Array.append⟩ partial def isEqvAux (a b : Array α) (hsz : a.size = b.size) (p : α → α → Bool) : Nat → Bool | i := if h : i < a.size then - let aidx : Fin a.size := ⟨i, h⟩ in - let bidx : Fin b.size := ⟨i, hsz ▸ h⟩ in + let aidx : Fin a.size := ⟨i, h⟩; + let bidx : Fin b.size := ⟨i, hsz ▸ h⟩; match p (a.fget aidx) (b.fget bidx) with | true := isEqvAux (i+1) | false := false @@ -359,11 +359,11 @@ instance [HasBeq α] : HasBeq (Array α) := -- TODO(Leo): justify termination using wf-rec, and use `fswap` partial def reverseAux : Array α → Nat → Array α | a i := - let n := a.size in + let n := a.size; if i < n / 2 then - reverseAux (a.swap i (n - i - 1)) (i+1) + reverseAux (a.swap i (n - i - 1)) (i+1) else - a + a def reverse (a : Array α) : Array α := reverseAux a 0 diff --git a/library/init/data/array/binsearch.lean b/library/init/data/array/binsearch.lean index f1c96d4a43..5f1111a3d1 100644 --- a/library/init/data/array/binsearch.lean +++ b/library/init/data/array/binsearch.lean @@ -14,8 +14,8 @@ namespace Array @[specialize] partial def binSearchAux {α : Type u} {β : Type v} [Inhabited α] [Inhabited β] (lt : α → α → Bool) (found : Option α → β) (as : Array α) (k : α) : Nat → Nat → β | lo hi := if lo <= hi then - let m := (lo + hi)/2 in - let a := as.get m in + let m := (lo + hi)/2; + let a := as.get m; if lt a k then binSearchAux (m+1) hi else if lt k a then if m == 0 then found none diff --git a/library/init/data/array/qsort.lean b/library/init/data/array/qsort.lean index 3d68ce1a89..719edd140b 100644 --- a/library/init/data/array/qsort.lean +++ b/library/init/data/array/qsort.lean @@ -14,30 +14,30 @@ namespace Array | as i j := if j < hi then if lt (as.get j) pivot then - let as := as.swap i j in + let as := as.swap i j; partitionAux as (i+1) (j+1) else partitionAux as i (j+1) else - let as := as.swap i hi in + let as := as.swap i hi; (i, as) @[inline] def partition {α : Type} [Inhabited α] (as : Array α) (lt : α → α → Bool) (lo hi : Nat) : Nat × Array α := -let mid := (lo + hi) / 2 in -let as := if lt (as.get mid) (as.get lo) then as.swap lo mid else as in -let as := if lt (as.get hi) (as.get lo) then as.swap lo hi else as in -let as := if lt (as.get mid) (as.get hi) then as.swap mid hi else as in -let pivot := as.get hi in +let mid := (lo + hi) / 2; +let as := if lt (as.get mid) (as.get lo) then as.swap lo mid else as; +let as := if lt (as.get hi) (as.get lo) then as.swap lo hi else as; +let as := if lt (as.get mid) (as.get hi) then as.swap mid hi else as; +let pivot := as.get hi; partitionAux lt hi pivot as lo lo @[specialize] partial def qsortAux {α : Type} [Inhabited α] (lt : α → α → Bool) : Array α → Nat → Nat → Array α | as low high := if low < high then - let p := partition as lt low high in + let p := partition as lt low high; -- TODO: fix `partial` support in the equation compiler, it breaks if we use `let (mid, as) := partition as lt low high` - let mid := p.1 in - let as := p.2 in - let as := qsortAux as low mid in + let mid := p.1; + let as := p.2; + let as := qsortAux as low mid; qsortAux as (mid+1) high else as diff --git a/library/init/data/char/basic.lean b/library/init/data/char/basic.lean index 1da691a6c0..06034cd01a 100644 --- a/library/init/data/char/basic.lean +++ b/library/init/data/char/basic.lean @@ -18,7 +18,7 @@ instance : HasSizeof Char := namespace Char def utf8Size (c : Char) : UInt32 := -let v := c.val in +let v := c.val; if UInt32.land v 0x80 = 0 then 1 else if UInt32.land v 0xE0 = 0xC0 then 2 else if UInt32.land v 0xF0 = 0xE0 then 3 @@ -88,7 +88,7 @@ def isAlphanum (c : Char) : Bool := c.isAlpha || c.isDigit def toLower (c : Char) : Char := -let n := toNat c in +let n := toNat c; if n >= 65 ∧ n <= 90 then ofNat (n + 32) else c end Char diff --git a/library/init/data/hashmap/basic.lean b/library/init/data/hashmap/basic.lean index 143d7966f8..aaf91eecb2 100644 --- a/library/init/data/hashmap/basic.lean +++ b/library/init/data/hashmap/basic.lean @@ -20,7 +20,7 @@ structure HashMapImp (α : Type u) (β : Type v) := (buckets : HashMapBucket α β) def mkHashMapImp {α : Type u} {β : Type v} (nbuckets := 8) : HashMapImp α β := -let n := if nbuckets = 0 then 8 else nbuckets in +let n := if nbuckets = 0 then 8 else nbuckets; { size := 0, buckets := ⟨ mkArray n AssocList.nil, @@ -39,7 +39,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 : HashMapBucket α β) (a : α) (b : β) : HashMapBucket α β := -let ⟨i, h⟩ := mkIdx data.property (hashFn a) in +let ⟨i, h⟩ := mkIdx data.property (hashFn a); data.update i (AssocList.cons a b (data.val.uget i h)) h @[inline] def mfoldBuckets {δ : Type w} {m : Type w → Type w} [Monad m] (data : HashMapBucket α β) (d : δ) (f : δ → α → β → m δ) : m δ := @@ -57,45 +57,45 @@ foldBuckets m.buckets d f def find [HasBeq α] [Hashable α] (m : HashMapImp α β) (a : α) : Option β := match m with | ⟨_, buckets⟩ := - let ⟨i, h⟩ := mkIdx buckets.property (hash a) in + let ⟨i, h⟩ := mkIdx buckets.property (hash a); (buckets.val.uget i h).find a def contains [HasBeq α] [Hashable α] (m : HashMapImp α β) (a : α) : Bool := match m with | ⟨_, buckets⟩ := - let ⟨i, h⟩ := mkIdx buckets.property (hash a) in + 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 (AssocList α β) → HashMapBucket α β → HashMapBucket α β | i source target := if h : i < source.size then - let idx : Fin source.size := ⟨i, h⟩ in - let es : AssocList α β := source.fget idx in + let idx : Fin source.size := ⟨i, h⟩; + let es : AssocList α β := source.fget idx; -- We remove `es` from `source` to make sure we can reuse its memory cells when performing es.foldl - let source := source.fset idx AssocList.nil in - let target := es.foldl (reinsertAux hash) target in + let source := source.fset idx AssocList.nil; + let target := es.foldl (reinsertAux hash) target; moveEntries (i+1) source target else target def expand [Hashable α] (size : Nat) (buckets : HashMapBucket α β) : HashMapImp α β := -let nbuckets := buckets.val.size * 2 in +let nbuckets := buckets.val.size * 2; have aux₁ : nbuckets > 0, from Nat.mulPos buckets.property (Nat.zeroLtBit0 Nat.oneNeZero), have aux₂ : (mkArray nbuckets (@AssocList.nil α β)).size = nbuckets, from Array.szMkArrayEq _ _, -let new_buckets : HashMapBucket α β := ⟨mkArray nbuckets AssocList.nil, aux₂.symm ▸ aux₁⟩ in +let new_buckets : HashMapBucket α β := ⟨mkArray nbuckets AssocList.nil, aux₂.symm ▸ aux₁⟩; { size := size, buckets := moveEntries 0 buckets.val new_buckets } def insert [HasBeq α] [Hashable α] (m : HashMapImp α β) (a : α) (b : β) : HashMapImp α β := match m with | ⟨size, buckets⟩ := - let ⟨i, h⟩ := mkIdx buckets.property (hash a) in - let bkt := buckets.val.uget i h in + 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 b) h⟩ else - let size' := size + 1 in - let buckets' := buckets.update i (AssocList.cons a b bkt) h in + let size' := size + 1; + let buckets' := buckets.update i (AssocList.cons a b bkt) h; if size' ≤ buckets.val.size then { size := size', buckets := buckets' } else expand size' buckets' @@ -103,8 +103,8 @@ match m with def erase [HasBeq α] [Hashable α] (m : HashMapImp α β) (a : α) : HashMapImp α β := match m with | ⟨ size, buckets ⟩ := - let ⟨i, h⟩ := mkIdx buckets.property (hash a) in - let bkt := buckets.val.uget i h in + 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 diff --git a/library/init/data/nat/bitwise.lean b/library/init/data/nat/bitwise.lean index 006dcf100c..efa91e7590 100644 --- a/library/init/data/nat/bitwise.lean +++ b/library/init/data/nat/bitwise.lean @@ -11,11 +11,11 @@ partial def bitwise (f : Bool → Bool → Bool) : Nat → Nat → Nat | n m := if n = 0 then (if f false true then m else 0) else if m = 0 then (if f true false then n else 0) else - let n' := n / 2 in - let m' := m / 2 in - let b₁ := n % 2 = 1 in - let b₂ := m % 2 = 1 in - let r := bitwise n' m' in + let n' := n / 2; + let m' := m / 2; + let b₁ := n % 2 = 1; + let b₂ := m % 2 = 1; + let r := bitwise n' m'; if f b₁ b₂ then bit1 r else bit0 r @[extern cpp "lean::nat_land"] diff --git a/library/init/data/persistentarray/basic.lean b/library/init/data/persistentarray/basic.lean index c9568f2e41..a968409553 100644 --- a/library/init/data/persistentarray/basic.lean +++ b/library/init/data/persistentarray/basic.lean @@ -56,9 +56,9 @@ else partial def setAux : PersistentArrayNode α → USize → USize → α → PersistentArrayNode α | (node cs) i shift a := - let j := div2Shift i shift in - let i := mod2Shift i shift in - let shift := shift - initShift in + let j := div2Shift i shift; + let i := mod2Shift i shift; + let shift := shift - initShift; node $ cs.modify j.toNat $ λ c, setAux c i shift a | (leaf cs) i _ a := leaf (cs.set i.toNat a) @@ -70,9 +70,9 @@ else @[specialize] partial def modifyAux [Inhabited α] (f : α → α) : PersistentArrayNode α → USize → USize → PersistentArrayNode α | (node cs) i shift := - let j := div2Shift i shift in - let i := mod2Shift i shift in - let shift := shift - initShift in + let j := div2Shift i shift; + let i := mod2Shift i shift; + let shift := shift - initShift; node $ cs.modify j.toNat $ λ c, modifyAux c i shift | (leaf cs) i _ := leaf (cs.modify i.toNat f) @@ -94,9 +94,9 @@ partial def insertNewLeaf : PersistentArrayNode α → USize → USize → Array if i < branching then node (cs.push (leaf a)) else - let j := div2Shift i shift in - let i := mod2Shift i shift in - let shift := shift - initShift in + let j := div2Shift i shift; + let i := mod2Shift i shift; + let shift := shift - initShift; if j.toNat < cs.size then node $ cs.modify j.toNat $ λ c, insertNewLeaf c i shift a else @@ -110,7 +110,7 @@ if t.size <= (mul2Shift 1 (t.shift + initShift)).toNat then .. t } else { tail := Array.empty, - root := let n := mkEmptyArray.push t.root in + root := let n := mkEmptyArray.push t.root; node (n.push (mkNewPath t.shift t.tail)), shift := t.shift + initShift, tailOff := t.size, @@ -119,7 +119,7 @@ else def tooBig : Nat := usizeSz / 8 def push (t : PersistentArray α) (a : α) : PersistentArray α := -let r := { tail := t.tail.push a, size := t.size + 1, .. t } in +let r := { tail := t.tail.push a, size := t.size + 1, .. t }; if r.tail.size < branching.toNat || t.size >= tooBig then r else diff --git a/library/init/data/random.lean b/library/init/data/random.lean index e5f026fb55..20e64f3427 100644 --- a/library/init/data/random.lean +++ b/library/init/data/random.lean @@ -38,23 +38,23 @@ instance : HasRepr StdGen := def stdNext : StdGen → Nat × StdGen | ⟨s1, s2⟩ := - let k : Int := s1 / 53668 in - let s1' : Int := 40014 * ((s1 : Int) - k * 53668) - k * 12211 in - let s1'' : Int := if s1' < 0 then s1' + 2147483563 else s1' in - let k' : Int := s2 / 52774 in - let s2' : Int := 40692 * ((s2 : Int) - k' * 52774) - k' * 3791 in - let s2'' : Int := if s2' < 0 then s2' + 2147483399 else s2' in - let z : Int := s1'' - s2'' in - let z' : Int := if z < 1 then z + 2147483562 else z % 2147483562 in + let k : Int := s1 / 53668; + let s1' : Int := 40014 * ((s1 : Int) - k * 53668) - k * 12211; + let s1'' : Int := if s1' < 0 then s1' + 2147483563 else s1'; + let k' : Int := s2 / 52774; + let s2' : Int := 40692 * ((s2 : Int) - k' * 52774) - k' * 3791; + let s2'' : Int := if s2' < 0 then s2' + 2147483399 else s2'; + let z : Int := s1'' - s2''; + let z' : Int := if z < 1 then z + 2147483562 else z % 2147483562; (z'.toNat, ⟨s1''.toNat, s2''.toNat⟩) def stdSplit : StdGen → StdGen × StdGen | g@⟨s1, s2⟩ := - let newS1 := if s1 = 2147483562 then 1 else s1 + 1 in - let newS2 := if s2 = 1 then 2147483398 else s2 - 1 in - let newG := (stdNext g).2 in - let leftG := StdGen.mk newS1 newG.2 in - let rightG := StdGen.mk newG.1 newS2 in + let newS1 := if s1 = 2147483562 then 1 else s1 + 1; + let newS2 := if s2 = 1 then 2147483398 else s2 - 1; + let newG := (stdNext g).2; + let leftG := StdGen.mk newS1 newG.2; + let rightG := StdGen.mk newG.1 newS2; (leftG, rightG) instance : RandomGen StdGen := @@ -64,9 +64,9 @@ instance : RandomGen StdGen := /-- Return a standard number generator. -/ def mkStdGen (s : Nat := 0) : StdGen := -let q := s / 2147483562 in -let s1 := s % 2147483562 in -let s2 := q % 2147483398 in +let q := s / 2147483562; +let s1 := s % 2147483562; +let s2 := q % 2147483398; ⟨s1 + 1, s2 + 1⟩ /- @@ -78,31 +78,31 @@ The parameter `r` is the "remaining" magnitude. private partial def randNatAux {gen : Type u} [RandomGen gen] (genLo genMag : Nat) : Nat → (Nat × gen) → Nat × gen | 0 (v, g) := (v, g) | r'@(r+1) (v, g) := - let (x, g') := RandomGen.next g in - let v' := v*genMag + (x - genLo) in + let (x, g') := RandomGen.next g; + let v' := v*genMag + (x - genLo); randNatAux (r' / genMag - 1) (v', g') /-- Generate a random natural number in the interval [lo, hi]. -/ def randNat {gen : Type u} [RandomGen gen] (g : gen) (lo hi : Nat) : Nat × gen := -let lo' := if lo > hi then hi else lo in -let hi' := if lo > hi then lo else hi in -let (genLo, genHi) := RandomGen.range g in -let genMag := genHi - genLo + 1 in +let lo' := if lo > hi then hi else lo; +let hi' := if lo > hi then lo else hi; +let (genLo, genHi) := RandomGen.range g; +let genMag := genHi - genLo + 1; /- Probabilities of the most likely and least likely result will differ at most by a factor of (1 +- 1/q). Assuming the RandomGen is uniform, of course -/ -let q := 1000 in -let k := hi' - lo' + 1 in -let tgtMag := k * q in -let (v, g') := randNatAux genLo genMag tgtMag (0, g) in -let v' := lo' + (v % k) in +let q := 1000; +let k := hi' - lo' + 1; +let tgtMag := k * q; +let (v, g') := randNatAux genLo genMag tgtMag (0, g); +let v' := lo' + (v % k); (v', g') /-- Generate a random Boolean. -/ def randBool {gen : Type u} [RandomGen gen] (g : gen) : Bool × gen := -let (v, g') := randNat g 0 1 in +let (v, g') := randNat g 0 1; (v = 1, g') def IO.mkStdGenRef : IO (IO.Ref StdGen) := diff --git a/library/init/data/rbmap/basic.lean b/library/init/data/rbmap/basic.lean index 3eff7594b6..a555f89d01 100644 --- a/library/init/data/rbmap/basic.lean +++ b/library/init/data/rbmap/basic.lean @@ -166,7 +166,7 @@ variables (lt : α → α → Bool) else appendTrees a b @[specialize] def erase (x : α) (t : RBNode α β) : RBNode α β := -let t := del lt x t in +let t := del lt x t; t.setBlack end Erase diff --git a/library/init/data/repr.lean b/library/init/data/repr.lean index db40421376..7c1db01403 100644 --- a/library/init/data/repr.lean +++ b/library/init/data/repr.lean @@ -78,8 +78,8 @@ if n = 0xf then 'f' else def toDigitsCore (base : Nat) : Nat → Nat → List Char → List Char | 0 n ds := ds | (fuel+1) n ds := - let d := digitChar $ n % base in - let n' := n / base in + let d := digitChar $ n % base; + let n' := n / base; if n' = 0 then d::ds else toDigitsCore fuel n' (d::ds) @@ -98,9 +98,9 @@ def hexDigitRepr (n : Nat) : String := String.singleton $ Nat.digitChar n def charToHex (c : Char) : String := -let n := Char.toNat c in -let d2 := n / 16 in -let d1 := n % 16 in +let n := Char.toNat c; +let d2 := n / 16; +let d1 := n % 16; hexDigitRepr d2 ++ hexDigitRepr d1 def Char.quoteCore (c : Char) : String := diff --git a/library/init/data/string/basic.lean b/library/init/data/string/basic.lean index dde6d333e3..52d2b4afdb 100644 --- a/library/init/data/string/basic.lean +++ b/library/init/data/string/basic.lean @@ -95,14 +95,14 @@ def set : String → (@& Pos) → Char → String @[extern cpp "lean::string_utf8_next"] def next (s : @& String) (p : @& Pos) : Pos := -let c := get s p in +let c := get s p; p + csize c private def utf8PrevAux : List Char → Pos → Pos → Pos | [] i p := 0 | (c::cs) i p := - let cz := csize c in - let i' := i + cz in + let cz := csize c; + let i' := i + cz; if i' = p then i else utf8PrevAux cs i' p @[extern cpp "lean::string_utf8_prev"] @@ -146,11 +146,11 @@ def extract : (@& String) → (@& Pos) → (@& Pos) → String partial def splitAux (s sep : String) : Pos → Pos → Pos → List String → List String | b i j r := if s.atEnd i then - let r := if sep.atEnd j then ""::(s.extract b (i-j))::r else (s.extract b i)::r - in r.reverse + let r := if sep.atEnd j then ""::(s.extract b (i-j))::r else (s.extract b i)::r; + r.reverse else if s.get i == sep.get j then - let i := s.next i in - let j := sep.next j in + let i := s.next i; + let j := sep.next j; if sep.atEnd j then splitAux i i 0 (s.extract b (i-j)::r) else splitAux b i j r else splitAux b (s.next i) 0 r @@ -250,9 +250,10 @@ end Iterator private partial def lineColumnAux (s : String) : Pos → Nat × Nat → Nat × Nat | i r@(line, col) := if atEnd s i then r - else let c := s.get i in - if c = '\n' then lineColumnAux (s.next i) (line+1, 0) - else lineColumnAux (s.next i) (line, col+1) + else + let c := s.get i; + if c = '\n' then lineColumnAux (s.next i) (line+1, 0) + else lineColumnAux (s.next i) (line, col+1) def lineColumn (s : String) (pos : Pos) : Nat × Nat := lineColumnAux s 0 (1, 0) @@ -299,9 +300,10 @@ s.any (== c) @[specialize] partial def mapAux (f : Char → Char) : Pos → String → String | i s := if s.atEnd i then s - else let c := f (s.get i) in - let s := s.set i c in - mapAux (s.next i) s + else + let c := f (s.get i); + let s := s.set i c; + mapAux (s.next i) s @[inline] def map (f : Char → Char) (s : String) : String := mapAux f 0 s @@ -316,8 +318,8 @@ partial def isPrefixOfAux (p s : String) : Pos → Bool | i := if p.atEnd i then true else - let c₁ := p.get i in - let c₂ := s.get i in + let c₁ := p.get i; + let c₂ := s.get i; c₁ == c₂ && isPrefixOfAux (s.next i) /- Return true iff `p` is a prefix of `s` -/ @@ -339,7 +341,7 @@ namespace Substring @[inline] def next : Substring → String.Pos → String.Pos | ⟨s, b, e⟩ p := - let p := s.next (b+p) in + let p := s.next (b+p); if p > e then e - b else p - b @[inline] def prev : Substring → String.Pos → String.Pos @@ -365,12 +367,12 @@ match s with @[inline] def take : Substring → Nat → Substring | ⟨s, b, e⟩ n := - let e := if b + n ≥ e then e else b + n in + let e := if b + n ≥ e then e else b + n; ⟨s, b, e⟩ @[inline] def takeRight : Substring → Nat → Substring | ⟨s, b, e⟩ n := - let b := if e - n ≤ b then b else e - n in + let b := if e - n ≤ b then b else e - n; ⟨s, b, e⟩ @[inline] def atEnd : Substring → String.Pos → Bool @@ -382,11 +384,11 @@ match s with partial def splitAux (s sep : String) (stopPos : String.Pos) : String.Pos → String.Pos → String.Pos → List Substring → List Substring | b i j r := if i == stopPos then - let r := if sep.atEnd j then "".toSubstring::{str := s, startPos := b, stopPos := i-j}::r else {str := s, startPos := b, stopPos := i}::r - in r.reverse + let r := if sep.atEnd j then "".toSubstring::{str := s, startPos := b, stopPos := i-j}::r else {str := s, startPos := b, stopPos := i}::r; + r.reverse else if s.get i == sep.get j then - let i := s.next i in - let j := sep.next j in + let i := s.next i; + let j := sep.next j; if sep.atEnd j then splitAux i i 0 ({str := s, startPos := b, stopPos := i-j}::r) else splitAux b i j r else splitAux b (s.next i) 0 r @@ -420,30 +422,31 @@ s.any (== c) @[inline] def takeWhile : Substring → (Char → Bool) → Substring | ⟨s, b, e⟩ p := - let e := takeWhileAux s e p b in + let e := takeWhileAux s e p b; ⟨s, b, e⟩ @[inline] def dropWhile : Substring → (Char → Bool) → Substring | ⟨s, b, e⟩ p := - let b := takeWhileAux s e p b in + let b := takeWhileAux s e p b; ⟨s, b, e⟩ @[specialize] partial def takeRightWhileAux (s : String) (begPos : String.Pos) (p : Char → Bool) : String.Pos → String.Pos | i := if i == begPos then i - else let i' := s.prev i in - let c := s.get i' in - if !p c then i - else takeRightWhileAux i' + else + let i' := s.prev i; + let c := s.get i'; + if !p c then i + else takeRightWhileAux i' @[inline] def takeRightWhile : Substring → (Char → Bool) → Substring | ⟨s, b, e⟩ p := - let b := takeRightWhileAux s b p e in + let b := takeRightWhileAux s b p e; ⟨s, b, e⟩ @[inline] def dropRightWhile : Substring → (Char → Bool) → Substring | ⟨s, b, e⟩ p := - let e := takeRightWhileAux s b p e in + let e := takeRightWhileAux s b p e; ⟨s, b, e⟩ @[inline] def trimLeft (s : Substring) : Substring := @@ -454,8 +457,8 @@ s.dropRightWhile Char.isWhitespace @[inline] def trim : Substring → Substring | ⟨s, b, e⟩ := - let b := takeWhileAux s e Char.isWhitespace b in - let e := takeRightWhileAux s b Char.isWhitespace e in + let b := takeWhileAux s e Char.isWhitespace b; + let e := takeRightWhileAux s b Char.isWhitespace e; ⟨s, b, e⟩ def toNat (s : Substring) : Nat := diff --git a/library/init/lean/attributes.lean b/library/init/lean/attributes.lean index 48f8887e83..cffbb4f3f9 100644 --- a/library/init/lean/attributes.lean +++ b/library/init/lean/attributes.lean @@ -73,13 +73,13 @@ match (scopeManagerExt.getState env).headers with @[export lean.to_valid_namespace_core] def toValidNamespace (env : Environment) (n : Name) : Option Name := -let s := scopeManagerExt.getState env in +let s := scopeManagerExt.getState env; if s.allNamespaces.contains n then some n else s.namespaces.foldl (λ r ns, match r with | some _ := r | none := - let c := ns ++ n in + let c := ns ++ n; if s.allNamespaces.contains c then some c else none) none @@ -92,14 +92,14 @@ def registerNamespace : Environment → Name → Environment | env _ := env def pushScopeCore (env : Environment) (header : Name) (isNamespace : Bool) : Environment := -let ns := env.getNamespace in -let newNs := if isNamespace then ns ++ header else ns in -let env := env.registerNamespaceAux newNs in +let ns := env.getNamespace; +let newNs := if isNamespace then ns ++ header else ns; +let env := env.registerNamespaceAux newNs; let env := scopeManagerExt.modifyState env $ λ s, { headers := header :: s.headers, namespaces := newNs :: s.namespaces, isNamespace := isNamespace :: s.isNamespace, - .. s } in + .. s }; env def popScopeCore (env : Environment) : Environment := @@ -257,7 +257,7 @@ ext : PersistentEnvExtension Name NameSet ← registerPersistentEnvExtension { addImportedFn := λ _, {}, addEntryFn := λ (s : NameSet) n, s.insert n, exportEntriesFn := λ es, - let r : Array Name := es.fold (λ a e, a.push e) Array.empty in + let r : Array Name := es.fold (λ a e, a.push e) Array.empty; r.qsort Name.quickLt, statsFn := λ s, "tag attribute" ++ Format.line ++ "number of local entries: " ++ format s.size }, @@ -306,7 +306,7 @@ ext : PersistentEnvExtension (Name × α) (NameMap α) ← registerPersistentEnv addImportedFn := λ _, {}, addEntryFn := λ (s : NameMap α) (p : Name × α), s.insert p.1 p.2, exportEntriesFn := λ m, - let r : Array (Name × α) := m.fold (λ a n p, a.push (n, p)) Array.empty in + let r : Array (Name × α) := m.fold (λ a n p, a.push (n, p)) Array.empty; r.qsort (λ a b, Name.quickLt a.1 b.1), statsFn := λ s, "parametric attribute" ++ Format.line ++ "number of local entries: " ++ format s.size }, @@ -365,7 +365,7 @@ ext : PersistentEnvExtension (Name × α) (NameMap α) ← registerPersistentEnv addImportedFn := λ _, {}, addEntryFn := λ (s : NameMap α) (p : Name × α), s.insert p.1 p.2, exportEntriesFn := λ m, - let r : Array (Name × α) := m.fold (λ a n p, a.push (n, p)) Array.empty in + let r : Array (Name × α) := m.fold (λ a n p, a.push (n, p)) Array.empty; r.qsort (λ a b, Name.quickLt a.1 b.1), statsFn := λ s, "enumeration attribute extension" ++ Format.line ++ "number of local entries: " ++ format s.size }, diff --git a/library/init/lean/compiler/closedtermcache.lean b/library/init/lean/compiler/closedtermcache.lean index 5933ae72dd..81925e50db 100644 --- a/library/init/lean/compiler/closedtermcache.lean +++ b/library/init/lean/compiler/closedtermcache.lean @@ -14,7 +14,7 @@ def mkClosedTermCacheExtension : IO (SimplePersistentEnvExtension (Expr × Name) registerSimplePersistentEnvExtension { name := `closedTermCache, addImportedFn := λ as, - let cache : ClosedTermCache := mkStateFromImportedEntries (λ s (p : Expr × Name), s.insert p.1 p.2) {} as in + let cache : ClosedTermCache := mkStateFromImportedEntries (λ s (p : Expr × Name), s.insert p.1 p.2) {} as; cache.switch, addEntryFn := λ s ⟨e, n⟩, s.insert e n } diff --git a/library/init/lean/compiler/constfolding.lean b/library/init/lean/compiler/constfolding.lean index 1642329d64..cb77a681e3 100644 --- a/library/init/lean/compiler/constfolding.lean +++ b/library/init/lean/compiler/constfolding.lean @@ -130,8 +130,8 @@ def getBoolLit : Expr → Option Bool | _ := none def foldStrictAnd (_ : Bool) (a₁ a₂ : Expr) : Option Expr := -let v₁ := getBoolLit a₁ in -let v₂ := getBoolLit a₂ in +let v₁ := getBoolLit a₁; +let v₂ := getBoolLit a₂; match v₁, v₂ with | some true, _ := a₂ | some false, _ := a₁ @@ -140,8 +140,8 @@ match v₁, v₂ with | _, _ := none def foldStrictOr (_ : Bool) (a₁ a₂ : Expr) : Option Expr := -let v₁ := getBoolLit a₁ in -let v₂ := getBoolLit a₂ in +let v₁ := getBoolLit a₁; +let v₂ := getBoolLit a₂; match v₁, v₂ with | some true, _ := a₁ | some false, _ := a₂ diff --git a/library/init/lean/compiler/exportattr.lean b/library/init/lean/compiler/exportattr.lean index ea6fda55c5..f69173035e 100644 --- a/library/init/lean/compiler/exportattr.lean +++ b/library/init/lean/compiler/exportattr.lean @@ -9,7 +9,7 @@ import init.lean.attributes namespace Lean private def isValidCppId (id : String) : Bool := -let first := id.get 0 in +let first := id.get 0; first.isAlpha && (id.toSubstring.drop 1).all (λ c, c.isAlpha || c.isDigit || c == '_') private def isValidCppName : Name → Bool diff --git a/library/init/lean/compiler/externattr.lean b/library/init/lean/compiler/externattr.lean index 11b74250e6..e9337bbd87 100644 --- a/library/init/lean/compiler/externattr.lean +++ b/library/init/lean/compiler/externattr.lean @@ -43,12 +43,12 @@ private partial def syntaxToExternEntries (a : Array Syntax) : Nat → List Exte if i == a.size then Except.ok entries else match a.get i with | Syntax.ident _ _ backend _ _ := - let i := i + 1 in + let i := i + 1; if i == a.size then Except.error "string or identifier expected" else match (a.get i).isIdOrAtom with | some "adhoc" := syntaxToExternEntries (i+1) (ExternEntry.adhoc backend :: entries) | some "inline" := - let i := i + 1 in + let i := i + 1; match (a.get i).isStrLit with | some pattern := syntaxToExternEntries (i+1) (ExternEntry.inline backend pattern :: entries) | none := Except.error "string literal expected" @@ -65,7 +65,7 @@ match s with else let (arity, i) : Option Nat × Nat := match (args.get 0).isNatLit with | some arity := (some arity, 1) - | none := (none, 0) in + | none := (none, 0); match (args.get i).isStrLit with | some str := if args.size == i+1 then @@ -101,7 +101,7 @@ private def parseOptNum : Nat → String.Iterator → Nat → String.Iterator × | (n+1) it r := if !it.hasNext then (it, r) else - let c := it.curr in + let c := it.curr; if '0' <= c && c <= '9' then parseOptNum n it.next (r*10 + (c.toNat - '0'.toNat)) else (it, r) @@ -110,12 +110,12 @@ def expandExternPatternAux (args : List String) : Nat → String.Iterator → St | 0 it r := r | (i+1) it r := if ¬ it.hasNext then r - else let c := it.curr in + else let c := it.curr; if c ≠ '#' then expandExternPatternAux i it.next (r.push c) else - let it := it.next in - let (it, j) := parseOptNum it.remainingBytes it 0 in - let j := j-1 in + let it := it.next; + let (it, j) := parseOptNum it.remainingBytes it 0; + let j := j-1; expandExternPatternAux i it (r ++ (args.getOpt j).getOrElse "") def expandExternPattern (pattern : String) (args : List String) : String := diff --git a/library/init/lean/compiler/ir/basic.lean b/library/init/lean/compiler/ir/basic.lean index d615ca34a0..8f8422b1e5 100644 --- a/library/init/lean/compiler/ir/basic.lean +++ b/library/init/lean/compiler/ir/basic.lean @@ -298,8 +298,8 @@ b.setBody FnBody.nil /- If b is a non terminal, then return a pair `(c, b')` s.t. `b == c <;> b'`, and c.body == FnBody.nil -/ @[inline] def FnBody.split (b : FnBody) : FnBody × FnBody := -let b' := b.body in -let c := b.resetBody in +let b' := b.body; +let c := b.resetBody; (c, b') def AltCore.body : Alt → FnBody @@ -323,7 +323,7 @@ def Alt.isDefault : Alt → Bool | (Alt.default _) := true def push (bs : Array FnBody) (b : FnBody) : Array FnBody := -let b := b.resetBody in +let b := b.resetBody; bs.push b partial def flattenAux : FnBody → Array FnBody → (Array FnBody) × FnBody @@ -338,9 +338,9 @@ partial def reshapeAux : Array FnBody → Nat → FnBody → FnBody | a i b := if i == 0 then b else - let i := i - 1 in - let (curr, a) := a.swapAt i (default _) in - let b := curr.setBody b in + let i := i - 1; + let (curr, a) := a.swapAt i (default _); + let b := curr.setBody b; reshapeAux a i b def reshape (bs : Array FnBody) (term : FnBody) : FnBody := diff --git a/library/init/lean/compiler/ir/borrow.lean b/library/init/lean/compiler/ir/borrow.lean index b9f30de5d2..fdc0247141 100644 --- a/library/init/lean/compiler/ir/borrow.lean +++ b/library/init/lean/compiler/ir/borrow.lean @@ -43,9 +43,9 @@ def ParamMap.fmt (map : ParamMap) : Format := let fmts := map.fold (λ fmt k ps, let k := match k with | Key.decl n := format n - | Key.jp n id := format n ++ ":" ++ format id in + | Key.jp n id := format n ++ ":" ++ format id; fmt ++ Format.line ++ k ++ " -> " ++ formatParams ps) - Format.nil in + Format.nil; "{" ++ (Format.nest 1 fmts) ++ "}" instance : HasFormat ParamMap := ⟨ParamMap.fmt⟩ @@ -96,22 +96,22 @@ namespace ApplyParamMap partial def visitFnBody : FnBody → FunId → ParamMap → FnBody | (FnBody.jdecl j xs v b) fnid map := - let v := visitFnBody v fnid map in - let b := visitFnBody b fnid map in + let v := visitFnBody v fnid map; + let b := visitFnBody b fnid map; match map.find (Key.jp fnid j) with | some ys := FnBody.jdecl j ys v b | none := FnBody.jdecl j xs v b | e fnid map := if e.isTerminal then e else - let (instr, b) := e.split in - let b := visitFnBody b fnid map in + let (instr, b) := e.split; + let b := visitFnBody b fnid map; instr.setBody b def visitDecls (decls : Array Decl) (map : ParamMap) : Array Decl := decls.map $ λ decl, match decl with | Decl.fdecl f xs ty b := - let b := visitFnBody b f map in + let b := visitFnBody b f map; match map.find (Key.decl f) with | some xs := Decl.fdecl f xs ty b | none := Decl.fdecl f xs ty b @@ -279,7 +279,7 @@ whileModifingOwnedAux x () partial def collectDecl : Decl → M Unit | (Decl.fdecl f ys _ b) := - adaptReader (λ ctx, let ctx := updateParamSet ctx ys in { currFn := f, .. ctx }) $ do + adaptReader (λ ctx, let ctx := updateParamSet ctx ys; { currFn := f, .. ctx }) $ do modify $ λ s : BorrowInfState, { owned := {}, .. s }, whileModifingOwned (collectFnBody b), updateParamMap (Key.decl f) diff --git a/library/init/lean/compiler/ir/boxing.lean b/library/init/lean/compiler/ir/boxing.lean index c6f0b832f3..b0640374ea 100644 --- a/library/init/lean/compiler/ir/boxing.lean +++ b/library/init/lean/compiler/ir/boxing.lean @@ -40,7 +40,7 @@ do idx ← get, pure {idx := idx } def requiresBoxedVersion (env : Environment) (decl : Decl) : Bool := -let ps := decl.params in +let ps := decl.params; ps.size > 0 && (decl.resultType.isScalar || ps.any (λ p, p.ty.isScalar || p.borrow) || isExtern env decl.name) def mkBoxedVersionAux (decl : Decl) : N Decl := @@ -49,9 +49,9 @@ let ps := decl.params, qs ← ps.mmap (λ _, do x ← mkFresh, pure { Param . x := x, ty := IRType.object, borrow := false }), (newVDecls, xs) ← qs.size.mfold (λ i (r : Array FnBody × Array Arg), - let (newVDecls, xs) := r in - let p := ps.get i in - let q := qs.get i in + let (newVDecls, xs) := r; + let p := ps.get i; + let q := qs.get i; if !p.ty.isScalar then pure (newVDecls, xs.push (Arg.var q.x)) else do x ← mkFresh, @@ -75,7 +75,7 @@ def mkBoxedVersion (decl : Decl) : Decl := def addBoxedVersions (env : Environment) (decls : Array Decl) : Array Decl := let boxedDecls := decls.foldl (λ (newDecls : Array Decl) decl, if requiresBoxedVersion env decl then newDecls.push (mkBoxedVersion decl) else newDecls) - Array.empty in + Array.empty; decls ++ boxedDecls @[export lean.ir.add_boxed_version_core] @@ -92,11 +92,11 @@ let isScalar := alts.size > 1 && -- Recall that we encode Unit and PUnit using `object`. alts.all (λ alt, match alt with | Alt.ctor c _ := c.isScalar - | Alt.default _ := false) in + | Alt.default _ := false); match isScalar with | false := IRType.object | true := - let n := alts.size in + let n := alts.size; if n < 256 then IRType.uint8 else if n < 65536 then IRType.uint16 else if n < 4294967296 then IRType.uint32 @@ -164,8 +164,8 @@ match x with @[specialize] def castArgsIfNeededAux (xs : Array Arg) (typeFromIdx : Nat → IRType) : M (Array Arg × Array FnBody) := xs.miterate (Array.empty, Array.empty) $ λ i (x : Arg) (r : Array Arg × Array FnBody), - let expected := typeFromIdx i.val in - let (xs, bs) := r in + let expected := typeFromIdx i.val; + let (xs, bs) := r; match x with | Arg.irrelevant := pure (xs.push x, bs) | Arg.var x := do @@ -257,13 +257,13 @@ partial def visitFnBody : FnBody → M FnBody pure other def run (env : Environment) (decls : Array Decl) : Array Decl := -let ctx : BoxingContext := { decls := decls, env := env } in +let ctx : BoxingContext := { decls := decls, env := env }; let decls := decls.map (λ decl, match decl with | Decl.fdecl f xs t b := - let nextIdx := decl.maxIndex + 1 in - let b := (withParams xs (visitFnBody b) { resultType := t, .. ctx }).run' nextIdx in + let nextIdx := decl.maxIndex + 1; + let b := (withParams xs (visitFnBody b) { resultType := t, .. ctx }).run' nextIdx; Decl.fdecl f xs t b - | d := d) in + | d := d); addBoxedVersions env decls end ExplicitBoxing diff --git a/library/init/lean/compiler/ir/compilerm.lean b/library/init/lean/compiler/ir/compilerm.lean index f88ea4106f..504bbbb811 100644 --- a/library/init/lean/compiler/ir/compilerm.lean +++ b/library/init/lean/compiler/ir/compilerm.lean @@ -74,15 +74,15 @@ abbrev DeclMap := SMap Name Decl Name.quickLt `decls` may contain duplicate entries, but we assume the one that occurs last is the most recent one. -/ private def mkEntryArray (decls : List Decl) : Array Decl := /- Remove duplicates by adding decls into a map -/ -let map : HashMap Name Decl := {} in -let map := decls.foldl (λ (map : HashMap Name Decl) decl, map.insert decl.name decl) map in +let map : HashMap Name Decl := {}; +let map := decls.foldl (λ (map : HashMap Name Decl) decl, map.insert decl.name decl) map; map.fold (λ a k v, a.push v) Array.empty def mkDeclMapExtension : IO (SimplePersistentEnvExtension Decl DeclMap) := registerSimplePersistentEnvExtension { name := `IRDecls, addImportedFn := λ as, - let m : DeclMap := mkStateFromImportedEntries (λ s (d : Decl), s.insert d.name d) {} as in + let m : DeclMap := mkStateFromImportedEntries (λ s (d : Decl), s.insert d.name d) {} as; m.switch, addEntryFn := λ s d, s.insert d.name d, toArrayFn := mkEntryArray diff --git a/library/init/lean/compiler/ir/elimdead.lean b/library/init/lean/compiler/ir/elimdead.lean index 117f612969..6351c48d43 100644 --- a/library/init/lean/compiler/ir/elimdead.lean +++ b/library/init/lean/compiler/ir/elimdead.lean @@ -14,15 +14,15 @@ partial def reshapeWithoutDeadAux : Array FnBody → FnBody → IndexSet → FnB | bs b used := if bs.isEmpty then b else - let curr := bs.back in - let bs := bs.pop in + let curr := bs.back; + let bs := bs.pop; let keep (_ : Unit) := - let used := curr.collectFreeIndices used in - let b := curr.setBody b in - reshapeWithoutDeadAux bs b used in + let used := curr.collectFreeIndices used; + let b := curr.setBody b; + reshapeWithoutDeadAux bs b used; let keepIfUsed (vidx : Index) := if used.contains vidx then keep () - else reshapeWithoutDeadAux bs b used in + else reshapeWithoutDeadAux bs b used; match curr with | FnBody.vdecl x _ _ _ := keepIfUsed x.idx | FnBody.jdecl j _ _ _ := keepIfUsed j.idx @@ -33,13 +33,13 @@ reshapeWithoutDeadAux bs term term.freeIndices partial def FnBody.elimDead : FnBody → FnBody | b := - let (bs, term) := b.flatten in - let bs := modifyJPs bs FnBody.elimDead in + let (bs, term) := b.flatten; + let bs := modifyJPs bs FnBody.elimDead; let term := match term with | FnBody.case tid x alts := - let alts := alts.map $ λ alt, alt.modifyBody FnBody.elimDead in + let alts := alts.map $ λ alt, alt.modifyBody FnBody.elimDead; FnBody.case tid x alts - | other := other in + | other := other; reshapeWithoutDead bs term /-- Eliminate dead let-declarations and join points -/ diff --git a/library/init/lean/compiler/ir/emitcpp.lean b/library/init/lean/compiler/ir/emitcpp.lean index 84282e7a42..6e5bf0e951 100644 --- a/library/init/lean/compiler/ir/emitcpp.lean +++ b/library/init/lean/compiler/ir/emitcpp.lean @@ -486,7 +486,7 @@ def toHexDigit (c : Nat) : String := String.singleton c.digitChar def quoteString (s : String) : String := -let q := "\"" in +let q := "\""; let q := s.foldl (λ q c, q ++ if c == '\n' then "\\n" @@ -496,7 +496,7 @@ let q := s.foldl else if c.toNat <= 255 && (c.toNat <= 31 || c.toNat >= 0x7f) then "\\x" ++ toHexDigit (c.toNat / 16) ++ toHexDigit (c.toNat % 16) else String.singleton c ) - q in + q; q ++ "\"" def emitNumLit (t : IRType) (v : Nat) : M Unit := @@ -559,9 +559,9 @@ That is, we have ``` -/ def overwriteParam (ps : Array Param) (ys : Array Arg) : Bool := -let n := ps.size in +let n := ps.size; n.any $ λ i, - let p := ps.get i in + let p := ps.get i; (i+1, n).anyI $ λ j, paramEqArg p (ys.get j) def emitTailCall (v : Expr) : M Unit := @@ -653,7 +653,7 @@ unless (hasInitAttr env d.name) $ | _ := pure () def emitDecl (d : Decl) : M Unit := -let d := d.normalizeIds in +let d := d.normalizeIds; catch (emitDeclAux d) (λ err, throw (err ++ "\ncompiling:\n" ++ toString d)) diff --git a/library/init/lean/compiler/ir/emitutil.lean b/library/init/lean/compiler/ir/emitutil.lean index 386f92e245..bbc0f863bc 100644 --- a/library/init/lean/compiler/ir/emitutil.lean +++ b/library/init/lean/compiler/ir/emitutil.lean @@ -38,7 +38,7 @@ partial def visitFnBody : FnBody → M Bool match findEnvDecl env f with | some (Decl.fdecl _ _ _ fbody) := visitFnBody fbody <||> visitFnBody b | other := visitFnBody b - } in + }; match v with | Expr.fap f _ := checkFn f | Expr.pap f _ := checkFn f diff --git a/library/init/lean/compiler/ir/expandresetreuse.lean b/library/init/lean/compiler/ir/expandresetreuse.lean index a6697df1c0..65ddcfd308 100644 --- a/library/init/lean/compiler/ir/expandresetreuse.lean +++ b/library/init/lean/compiler/ir/expandresetreuse.lean @@ -57,17 +57,17 @@ abbrev Mask := Array (Option VarId) /- Auxiliary function for eraseProjIncFor -/ partial def eraseProjIncForAux (y : VarId) : Array FnBody → Mask → Array FnBody → Array FnBody × Mask | bs mask keep := - let done (_ : Unit) := (bs ++ keep.reverse, mask) in - let keepInstr (b : FnBody) := eraseProjIncForAux bs.pop mask (keep.push b) in + let done (_ : Unit) := (bs ++ keep.reverse, mask); + let keepInstr (b : FnBody) := eraseProjIncForAux bs.pop mask (keep.push b); if bs.size < 2 then done () else - let b := bs.back in + let b := bs.back; match b with | (FnBody.vdecl _ _ (Expr.sproj _ _ _) _) := keepInstr b | (FnBody.vdecl _ _ (Expr.uproj _ _) _) := keepInstr b | (FnBody.inc z n c _) := if n == 0 then done () else - let b' := bs.get (bs.size - 2) in + let b' := bs.get (bs.size - 2); match b' with | (FnBody.vdecl w _ (Expr.proj i x) _) := if w == z && y == x then @@ -78,10 +78,10 @@ partial def eraseProjIncForAux (y : VarId) : Array FnBody → Mask → Array FnB ``` We keep `proj`, and `inc` when `n > 1` -/ - let bs := bs.pop.pop in - let mask := mask.set i (some z) in - let keep := keep.push b' in - let keep := if n == 1 then keep else keep.push (FnBody.inc z (n-1) c FnBody.nil) in + let bs := bs.pop.pop; + let mask := mask.set i (some z); + let keep := keep.push b'; + let keep := if n == 1 then keep else keep.push (FnBody.inc z (n-1) c FnBody.nil); eraseProjIncForAux bs mask keep else done () | other := done () @@ -105,13 +105,13 @@ partial def reuseToCtor (x : VarId) : FnBody → FnBody | _ := FnBody.vdecl z t v (reuseToCtor b) | (FnBody.case tid y alts) := - let alts := alts.map $ λ alt, alt.modifyBody reuseToCtor in + let alts := alts.map $ λ alt, alt.modifyBody reuseToCtor; FnBody.case tid y alts | e := if e.isTerminal then e else - let (instr, b) := e.split in - let b := reuseToCtor b in + let (instr, b) := e.split; + let b := reuseToCtor b; instr.setBody b /- @@ -127,8 +127,8 @@ where `z_i`'s are the variables in `mask`, and `b'` is `b` where we removed `dec x` and replaced `reuse x ctor_i ...` with `ctor_i ...`. -/ def mkSlowPath (x y : VarId) (mask : Mask) (b : FnBody) : FnBody := -let b := reuseToCtor x b in -let b := FnBody.dec y 1 true b in +let b := reuseToCtor x b; +let b := FnBody.dec y 1 true b; mask.foldl (λ b m, match m with | some z := FnBody.inc z 1 true b @@ -187,13 +187,13 @@ partial def removeSelfSet (ctx : Context) : FnBody → FnBody if isSelfSSet ctx x n i y then removeSelfSet b else FnBody.sset x n i y t (removeSelfSet b) | (FnBody.case tid y alts) := - let alts := alts.map $ λ alt, alt.modifyBody removeSelfSet in + let alts := alts.map $ λ alt, alt.modifyBody removeSelfSet; FnBody.case tid y alts | e := if e.isTerminal then e else - let (instr, b) := e.split in - let b := removeSelfSet b in + let (instr, b) := e.split; + let b := removeSelfSet b; instr.setBody b partial def reuseToSet (ctx : Context) (x y : VarId) : FnBody → FnBody @@ -204,19 +204,19 @@ partial def reuseToSet (ctx : Context) (x y : VarId) : FnBody → FnBody match v with | Expr.reuse w c u zs := if x == w then - let b := setFields y zs (b.replaceVar z y) in - let b := if u then FnBody.setTag y c.cidx b else b in + let b := setFields y zs (b.replaceVar z y); + let b := if u then FnBody.setTag y c.cidx b else b; removeSelfSet ctx b else FnBody.vdecl z t v (reuseToSet b) | _ := FnBody.vdecl z t v (reuseToSet b) | (FnBody.case tid y alts) := - let alts := alts.map $ λ alt, alt.modifyBody reuseToSet in + let alts := alts.map $ λ alt, alt.modifyBody reuseToSet; FnBody.case tid y alts | e := if e.isTerminal then e else - let (instr, b) := e.split in - let b := reuseToSet b in + let (instr, b) := e.split; + let b := reuseToSet b; instr.setBody b /- @@ -275,12 +275,12 @@ partial def searchAndExpand : FnBody → Array FnBody → M FnBody else searchAndExpand b.body (push bs b) def main (d : Decl) : Decl := -let d := d.normalizeIds in +let d := d.normalizeIds; match d with | (Decl.fdecl f xs t b) := - let m := mkProjMap d in - let nextIdx := d.maxIndex + 1 in - let b := (searchAndExpand b Array.empty { projMap := m }).run' nextIdx in + let m := mkProjMap d; + let nextIdx := d.maxIndex + 1; + let b := (searchAndExpand b Array.empty { projMap := m }).run' nextIdx; Decl.fdecl f xs t b | d := d diff --git a/library/init/lean/compiler/ir/format.lean b/library/init/lean/compiler/ir/format.lean index b8fa4a77c7..c2d549c17a 100644 --- a/library/init/lean/compiler/ir/format.lean +++ b/library/init/lean/compiler/ir/format.lean @@ -26,9 +26,9 @@ instance litValHasFormat : HasFormat LitVal := ⟨formatLitVal⟩ private def formatCtorInfo : CtorInfo → Format | { name := name, cidx := cidx, usize := usize, ssize := ssize, .. } := - let r := format "ctor_" ++ format cidx in - let r := if usize > 0 || ssize > 0 then r ++ "." ++ format usize ++ "." ++ format ssize else r in - let r := if name != Name.anonymous then r ++ "[" ++ format name ++ "]" else r in + let r := format "ctor_" ++ format cidx; + let r := if usize > 0 || ssize > 0 then r ++ "." ++ format usize ++ "." ++ format ssize else r; + let r := if name != Name.anonymous then r ++ "[" ++ format name ++ "]" else r; r instance ctorInfoHasFormat : HasFormat CtorInfo := ⟨formatCtorInfo⟩ diff --git a/library/init/lean/compiler/ir/livevars.lean b/library/init/lean/compiler/ir/livevars.lean index 39043d2a33..920935218b 100644 --- a/library/init/lean/compiler/ir/livevars.lean +++ b/library/init/lean/compiler/ir/livevars.lean @@ -131,8 +131,8 @@ def collectExpr : Expr → Collector partial def collectFnBody : FnBody → JPLiveVarMap → Collector | (FnBody.vdecl x _ v b) m := collectExpr v ∘ collectFnBody b m ∘ bindVar x | (FnBody.jdecl j ys v b) m := - let jLiveVars := (collectFnBody v m ∘ bindParams ys) {} in - let m := m.insert j jLiveVars in + let jLiveVars := (collectFnBody v m ∘ bindParams ys) {}; + let m := m.insert j jLiveVars; collectFnBody b m | (FnBody.set x _ y b) m := collectVar x ∘ collectArg y ∘ collectFnBody b m | (FnBody.setTag x _ b) m := collectVar x ∘ collectFnBody b m @@ -148,7 +148,7 @@ partial def collectFnBody : FnBody → JPLiveVarMap → Collector | (FnBody.jmp j xs) m := collectJP m j ∘ collectArgs xs def updateJPLiveVarMap (j : JoinPointId) (ys : Array Param) (v : FnBody) (m : JPLiveVarMap) : JPLiveVarMap := -let jLiveVars := (collectFnBody v m ∘ bindParams ys) {} in +let jLiveVars := (collectFnBody v m ∘ bindParams ys) {}; m.insert j jLiveVars end LiveVars diff --git a/library/init/lean/compiler/ir/pushproj.lean b/library/init/lean/compiler/ir/pushproj.lean index da9c07c1f5..d9c98cc73f 100644 --- a/library/init/lean/compiler/ir/pushproj.lean +++ b/library/init/lean/compiler/ir/pushproj.lean @@ -14,19 +14,19 @@ partial def pushProjs : Array FnBody → Array Alt → Array IndexSet → Array | bs alts altsF ctx ctxF := if bs.isEmpty then (ctx.reverse, alts) else - let b := bs.back in - let bs := bs.pop in - let done (_ : Unit) := (bs.push b ++ ctx.reverse, alts) in - let skip (_ : Unit) := pushProjs bs alts altsF (ctx.push b) (b.collectFreeIndices ctxF) in + let b := bs.back; + let bs := bs.pop; + let done (_ : Unit) := (bs.push b ++ ctx.reverse, alts); + let skip (_ : Unit) := pushProjs bs alts altsF (ctx.push b) (b.collectFreeIndices ctxF); let push (x : VarId) (t : IRType) (v : Expr) := if !ctxF.contains x.idx then let alts := alts.mapIdx $ λ i alt, alt.modifyBody $ λ b', if (altsF.get i).contains x.idx then b.setBody b' - else b' in - let altsF := altsF.map $ λ s, if s.contains x.idx then b.collectFreeIndices s else s in + else b'; + let altsF := altsF.map $ λ s, if s.contains x.idx then b.collectFreeIndices s else s; pushProjs bs alts altsF ctx ctxF else - skip () in + skip (); match b with | FnBody.vdecl x t v _ := match v with @@ -40,14 +40,14 @@ partial def pushProjs : Array FnBody → Array Alt → Array IndexSet → Array partial def FnBody.pushProj : FnBody → FnBody | b := - let (bs, term) := b.flatten in - let bs := modifyJPs bs FnBody.pushProj in + let (bs, term) := b.flatten; + let bs := modifyJPs bs FnBody.pushProj; match term with | FnBody.case tid x alts := - let altsF := alts.map $ λ alt, alt.body.freeIndices in - let (bs, alts) := pushProjs bs alts altsF Array.empty {x.idx} in - let alts := alts.map $ λ alt, alt.modifyBody FnBody.pushProj in - let term := FnBody.case tid x alts in + let altsF := alts.map $ λ alt, alt.body.freeIndices; + let (bs, alts) := pushProjs bs alts altsF Array.empty {x.idx}; + let alts := alts.map $ λ alt, alt.modifyBody FnBody.pushProj; + let term := FnBody.case tid x alts; reshape bs term | other := reshape bs term diff --git a/library/init/lean/compiler/ir/rc.lean b/library/init/lean/compiler/ir/rc.lean index 82c9d8fc64..2a736b941a 100644 --- a/library/init/lean/compiler/ir/rc.lean +++ b/library/init/lean/compiler/ir/rc.lean @@ -51,7 +51,7 @@ match ctx.jpLiveVarMap.find j with | none := {} def mustConsume (ctx : Context) (x : VarId) : Bool := -let info := getVarInfo ctx x in +let info := getVarInfo ctx x; info.ref && !info.persistent && info.consume @[inline] def addInc (x : VarId) (b : FnBody) (n := 1) : FnBody := @@ -62,7 +62,7 @@ FnBody.dec x 1 true b private def updateRefUsingCtorInfo (ctx : Context) (x : VarId) (c : CtorInfo) : Context := if c.isRef then ctx -else let m := ctx.varMap in +else let m := ctx.varMap; { varMap := match m.find x with | some info := m.insert x { ref := false, .. info } -- I really want a Lenses library + notation | none := m, @@ -75,7 +75,7 @@ caseLiveVars.fold /- `isFirstOcc xs x i = true` if `xs[i]` is the first occurrence of `xs[i]` in `xs` -/ private def isFirstOcc (xs : Array Arg) (i : Nat) : Bool := -let x := xs.get i in +let x := xs.get i; i.all $ λ j, xs.get j != x /- Return true if `x` also occurs in `ys` in a position that is not consumed. @@ -83,7 +83,7 @@ i.all $ λ j, xs.get j != x @[specialize] private def isBorrowParamAux (x : VarId) (ys : Array Arg) (consumeParamPred : Nat → Bool) : Bool := ys.size.any $ λ i, - let y := ys.get i in + let y := ys.get i; match y with | Arg.irrelevant := false | Arg.var y := x == y && !consumeParamPred i @@ -100,7 +100,7 @@ Return `n`, the number of times `x` is consumed. private def getNumConsumptions (x : VarId) (ys : Array Arg) (consumeParamPred : Nat → Bool) : Nat := ys.size.fold (λ i n, - let y := ys.get i in + let y := ys.get i; match y with | Arg.irrelevant := n | Arg.var y := if x == y && consumeParamPred i then n+1 else n) @@ -110,20 +110,20 @@ ys.size.fold private def addIncBeforeAux (ctx : Context) (xs : Array Arg) (consumeParamPred : Nat → Bool) (b : FnBody) (liveVarsAfter : LiveVarSet) : FnBody := xs.size.fold (λ i b, - let x := xs.get i in + let x := xs.get i; match x with | Arg.irrelevant := b | Arg.var x := - let info := getVarInfo ctx x in + let info := getVarInfo ctx x; if !info.ref || info.persistent || !isFirstOcc xs i then b else - let numConsuptions := getNumConsumptions x xs consumeParamPred in -- number of times the argument is + let numConsuptions := getNumConsumptions x xs consumeParamPred; -- number of times the argument is let numIncs := if !info.consume || -- `x` is not a variable that must be consumed by the current procedure liveVarsAfter.contains x || -- `x` is live after executing instruction isBorrowParamAux x xs consumeParamPred -- `x` is used in a position that is passed as a borrow reference then numConsuptions - else numConsuptions - 1 in + else numConsuptions - 1; -- dbgTrace ("addInc " ++ toString x ++ " nconsumptions: " ++ toString numConsuptions ++ " incs: " ++ toString numIncs -- ++ " consume: " ++ toString info.consume ++ " live: " ++ toString (liveVarsAfter.contains x) -- ++ " borrowParam : " ++ toString (isBorrowParamAux x xs consumeParamPred)) $ λ _, @@ -194,89 +194,89 @@ let b := match v with | (Expr.ctor _ ys) := addIncBeforeConsumeAll ctx ys (FnBody.vdecl z t v b) bLiveVars | (Expr.reuse _ _ _ ys) := addIncBeforeConsumeAll ctx ys (FnBody.vdecl z t v b) bLiveVars | (Expr.proj _ x) := - let b := addDecIfNeeded ctx x b bLiveVars in - let b := if (getVarInfo ctx x).consume then addInc z b else b in + let b := addDecIfNeeded ctx x b bLiveVars; + let b := if (getVarInfo ctx x).consume then addInc z b else b; (FnBody.vdecl z t v b) | (Expr.uproj _ x) := FnBody.vdecl z t v (addDecIfNeeded ctx x b bLiveVars) | (Expr.sproj _ _ x) := FnBody.vdecl z t v (addDecIfNeeded ctx x b bLiveVars) | (Expr.fap f ys) := -- dbgTrace ("processVDecl " ++ toString v) $ λ _, - let ps := (getDecl ctx f).params in - let b := addDecAfterFullApp ctx ys ps b bLiveVars in - let b := FnBody.vdecl z t v b in + let ps := (getDecl ctx f).params; + let b := addDecAfterFullApp ctx ys ps b bLiveVars; + let b := FnBody.vdecl z t v b; addIncBefore ctx ys ps b bLiveVars | (Expr.pap _ ys) := addIncBeforeConsumeAll ctx ys (FnBody.vdecl z t v b) bLiveVars | (Expr.ap x ys) := - let ysx := ys.push (Arg.var x) in -- TODO: avoid temporary array allocation + let ysx := ys.push (Arg.var x); -- TODO: avoid temporary array allocation addIncBeforeConsumeAll ctx ysx (FnBody.vdecl z t v b) bLiveVars | (Expr.unbox x) := FnBody.vdecl z t v (addDecIfNeeded ctx x b bLiveVars) - | other := FnBody.vdecl z t v b in -- Expr.reset, Expr.box, Expr.lit are handled here -let liveVars := updateLiveVars v bLiveVars in -let liveVars := liveVars.erase z in + | other := FnBody.vdecl z t v b; -- Expr.reset, Expr.box, Expr.lit are handled here +let liveVars := updateLiveVars v bLiveVars; +let liveVars := liveVars.erase z; (b, liveVars) def updateVarInfoWithParams (ctx : Context) (ps : Array Param) : Context := -let m := ps.foldl (λ (m : VarMap) p, m.insert p.x { ref := p.ty.isObj, consume := !p.borrow }) ctx.varMap in +let m := ps.foldl (λ (m : VarMap) p, m.insert p.x { ref := p.ty.isObj, consume := !p.borrow }) ctx.varMap; { varMap := m, .. ctx } partial def visitFnBody : FnBody → Context → (FnBody × LiveVarSet) | (FnBody.vdecl x t v b) ctx := - let ctx := updateVarInfo ctx x t v in - let (b, bLiveVars) := visitFnBody b ctx in + let ctx := updateVarInfo ctx x t v; + let (b, bLiveVars) := visitFnBody b ctx; processVDecl ctx x t v b bLiveVars | (FnBody.jdecl j xs v b) ctx := - let (v, vLiveVars) := visitFnBody v (updateVarInfoWithParams ctx xs) in - let v := addDecForDeadParams xs v vLiveVars in - let ctx := { jpLiveVarMap := updateJPLiveVarMap j xs v ctx.jpLiveVarMap, .. ctx } in - let (b, bLiveVars) := visitFnBody b ctx in + let (v, vLiveVars) := visitFnBody v (updateVarInfoWithParams ctx xs); + let v := addDecForDeadParams xs v vLiveVars; + let ctx := { jpLiveVarMap := updateJPLiveVarMap j xs v ctx.jpLiveVarMap, .. ctx }; + let (b, bLiveVars) := visitFnBody b ctx; (FnBody.jdecl j xs v b, bLiveVars) | (FnBody.uset x i y b) ctx := - let (b, s) := visitFnBody b ctx in + let (b, s) := visitFnBody b ctx; -- We don't need to insert `y` since we only need to track live variables that are references at runtime - let s := s.insert x in + let s := s.insert x; (FnBody.uset x i y b, s) | (FnBody.sset x i o y t b) ctx := - let (b, s) := visitFnBody b ctx in + let (b, s) := visitFnBody b ctx; -- We don't need to insert `y` since we only need to track live variables that are references at runtime - let s := s.insert x in + let s := s.insert x; (FnBody.sset x i o y t b, s) | (FnBody.mdata m b) ctx := - let (b, s) := visitFnBody b ctx in + let (b, s) := visitFnBody b ctx; (FnBody.mdata m b, s) | b@(FnBody.case tid x alts) ctx := - let caseLiveVars := collectLiveVars b ctx.jpLiveVarMap in + let caseLiveVars := collectLiveVars b ctx.jpLiveVarMap; let alts := alts.map $ λ alt, match alt with | Alt.ctor c b := - let ctx := updateRefUsingCtorInfo ctx x c in - let (b, altLiveVars) := visitFnBody b ctx in - let b := addDecForAlt ctx caseLiveVars altLiveVars b in + let ctx := updateRefUsingCtorInfo ctx x c; + let (b, altLiveVars) := visitFnBody b ctx; + let b := addDecForAlt ctx caseLiveVars altLiveVars b; Alt.ctor c b | Alt.default b := - let (b, altLiveVars) := visitFnBody b ctx in - let b := addDecForAlt ctx caseLiveVars altLiveVars b in - Alt.default b in + let (b, altLiveVars) := visitFnBody b ctx; + let b := addDecForAlt ctx caseLiveVars altLiveVars b; + Alt.default b; (FnBody.case tid x alts, caseLiveVars) | b@(FnBody.ret x) ctx := match x with | Arg.var x := - let info := getVarInfo ctx x in + let info := getVarInfo ctx x; if info.ref && !info.persistent && !info.consume then (addInc x b, {x}) else (b, {x}) | _ := (b, {}) | b@(FnBody.jmp j xs) ctx := - let jLiveVars := getJPLiveVars ctx j in - let ps := getJPParams ctx j in - let b := addIncBefore ctx xs ps b jLiveVars in - let bLiveVars := collectLiveVars b ctx.jpLiveVarMap in + let jLiveVars := getJPLiveVars ctx j; + let ps := getJPParams ctx j; + let b := addIncBefore ctx xs ps b jLiveVars; + let bLiveVars := collectLiveVars b ctx.jpLiveVarMap; (b, bLiveVars) | FnBody.unreachable _ := (FnBody.unreachable, {}) | other ctx := (other, {}) -- unreachable if well-formed partial def visitDecl (env : Environment) (decls : Array Decl) : Decl → Decl | (Decl.fdecl f xs t b) := - let ctx : Context := { env := env, decls := decls } in - let ctx := updateVarInfoWithParams ctx xs in - let (b, bLiveVars) := visitFnBody b ctx in - let b := addDecForDeadParams xs b bLiveVars in + let ctx : Context := { env := env, decls := decls }; + let ctx := updateVarInfoWithParams ctx xs; + let (b, bLiveVars) := visitFnBody b ctx; + let b := addDecForDeadParams xs b bLiveVars; Decl.fdecl f xs t b | other := other diff --git a/library/init/lean/compiler/ir/resetreuse.lean b/library/init/lean/compiler/ir/resetreuse.lean index c157178361..9100a12ebd 100644 --- a/library/init/lean/compiler/ir/resetreuse.lean +++ b/library/init/lean/compiler/ir/resetreuse.lean @@ -40,19 +40,19 @@ c₁.name.getPrefix == c₂.name.getPrefix private partial def S (w : VarId) (c : CtorInfo) : FnBody → FnBody | (FnBody.vdecl x t v@(Expr.ctor c' ys) b) := if mayReuse c c' then - let updtCidx := c.cidx != c'.cidx in + let updtCidx := c.cidx != c'.cidx; FnBody.vdecl x t (Expr.reuse w c' updtCidx ys) b else FnBody.vdecl x t v (S b) | (FnBody.jdecl j ys v b) := - let v' := S v in + let v' := S v; if v == v' then FnBody.jdecl j ys v (S b) else FnBody.jdecl j ys v' b | (FnBody.case tid x alts) := FnBody.case tid x $ alts.map $ λ alt, alt.modifyBody S | b := if b.isTerminal then b else let - (instr, b) := b.split in + (instr, b) := b.split; instr.setBody (S b) /- We use `Context` to track join points in scope. -/ @@ -64,7 +64,7 @@ do idx ← getModify (+1), private def tryS (x : VarId) (c : CtorInfo) (b : FnBody) : M FnBody := do w ← mkFresh, - let b' := S w c b in + let b' := S w c b, if b == b' then pure b else pure $ FnBody.vdecl w IRType.object (Expr.reset c.size x) b' @@ -155,8 +155,8 @@ open ResetReuse def Decl.insertResetReuse : Decl → Decl | d@(Decl.fdecl f xs t b) := - let nextIndex := d.maxIndex + 1 in - let b := (R b {}).run' nextIndex in + let nextIndex := d.maxIndex + 1; + let b := (R b {}).run' nextIndex; Decl.fdecl f xs t b | other := other diff --git a/library/init/lean/compiler/ir/simpcase.lean b/library/init/lean/compiler/ir/simpcase.lean index e42a7a061a..467e8972af 100644 --- a/library/init/lean/compiler/ir/simpcase.lean +++ b/library/init/lean/compiler/ir/simpcase.lean @@ -14,32 +14,32 @@ def ensureHasDefault (alts : Array Alt) : Array Alt := if alts.any Alt.isDefault then alts else if alts.size < 2 then alts else - let last := alts.back in - let alts := alts.pop in + let last := alts.back; + let alts := alts.pop; alts.push (Alt.default last.body) private def getOccsOf (alts : Array Alt) (i : Nat) : Nat := -let aBody := (alts.get i).body in +let aBody := (alts.get i).body; alts.iterateFrom 1 (i + 1) $ λ _ a' n, if a'.body == aBody then n+1 else n private def maxOccs (alts : Array Alt) : Alt × Nat := alts.iterateFrom (alts.get 0, getOccsOf alts 0) 1 $ λ i a p, - let noccs := getOccsOf alts i.val in + let noccs := getOccsOf alts i.val; if noccs > p.2 then (alts.fget i, noccs) else p private def addDefault (alts : Array Alt) : Array Alt := if alts.size <= 1 || alts.any Alt.isDefault then alts else - let (max, noccs) := maxOccs alts in + let (max, noccs) := maxOccs alts; if noccs == 1 then alts else - let alts := alts.filter $ (λ alt, alt.body != max.body) in + let alts := alts.filter $ (λ alt, alt.body != max.body); alts.push (Alt.default max.body) private def mkSimpCase (tid : Name) (x : VarId) (alts : Array Alt) : FnBody := -let alts := alts.filter (λ alt, alt.body != FnBody.unreachable) in -let alts := addDefault alts in +let alts := alts.filter (λ alt, alt.body != FnBody.unreachable); +let alts := addDefault alts; if alts.size == 0 then FnBody.unreachable else if alts.size == 1 then @@ -49,11 +49,11 @@ else partial def FnBody.simpCase : FnBody → FnBody | b := - let (bs, term) := b.flatten in - let bs := modifyJPs bs FnBody.simpCase in + let (bs, term) := b.flatten; + let bs := modifyJPs bs FnBody.simpCase; match term with | FnBody.case tid x alts := - let alts := alts.map $ λ alt, alt.modifyBody FnBody.simpCase in + let alts := alts.map $ λ alt, alt.modifyBody FnBody.simpCase; reshape bs (mkSimpCase tid x alts) | other := reshape bs term diff --git a/library/init/lean/compiler/namemangling.lean b/library/init/lean/compiler/namemangling.lean index 5d5900f57c..873e6993e6 100644 --- a/library/init/lean/compiler/namemangling.lean +++ b/library/init/lean/compiler/namemangling.lean @@ -10,26 +10,26 @@ namespace Lean private def String.mangleAux : Nat → String.Iterator → String → String | 0 it r := r | (i+1) it r := - let c := it.curr in + let c := it.curr; if c.isAlpha || c.isDigit then String.mangleAux i it.next (r.push c) else if c = '_' then String.mangleAux i it.next (r ++ "__") else if c.toNat < 255 then - let n := c.toNat in - let r := r ++ "_x" in - let r := r.push $ Nat.digitChar (n / 16) in - let r := r.push $ Nat.digitChar (n % 16) in + let n := c.toNat; + let r := r ++ "_x"; + let r := r.push $ Nat.digitChar (n / 16); + let r := r.push $ Nat.digitChar (n % 16); String.mangleAux i it.next r else - let n := c.toNat in - let r := r ++ "_u" in - let r := r.push $ Nat.digitChar (n / 4096) in - let n := n % 4096 in - let r := r.push $ Nat.digitChar (n / 256) in - let n := n % 256 in - let r := r.push $ Nat.digitChar (n / 16) in - let r := r.push $ Nat.digitChar (n % 16) in + let n := c.toNat; + let r := r ++ "_u"; + let r := r.push $ Nat.digitChar (n / 4096); + let n := n % 4096; + let r := r.push $ Nat.digitChar (n / 256); + let n := n % 256; + let r := r.push $ Nat.digitChar (n / 16); + let r := r.push $ Nat.digitChar (n % 16); String.mangleAux i it.next r def String.mangle (s : String) : String := @@ -38,7 +38,7 @@ String.mangleAux s.length s.mkIterator "" private def Name.mangleAux : Name → String | Name.anonymous := "" | (Name.mkString p s) := - let m := String.mangle s in + let m := String.mangle s; match p with | Name.anonymous := m | _ := Name.mangleAux p ++ "_" ++ m diff --git a/library/init/lean/compiler/util.lean b/library/init/lean/compiler/util.lean index e448c8f000..408502a654 100644 --- a/library/init/lean/compiler/util.lean +++ b/library/init/lean/compiler/util.lean @@ -52,7 +52,7 @@ end atMostOnce /-- Return true iff the free variable with id `x` occurs at most once in `e` -/ @[export lean.at_most_once_core] def atMostOnce (e : Expr) (x : Name) : Bool := -let {result := result, ..} := atMostOnce.visit x e {found := false, result := true} in +let {result := result, ..} := atMostOnce.visit x e {found := false, result := true}; result /- Helper functions for creating auxiliary names used in compiler passes. -/ diff --git a/library/init/lean/environment.lean b/library/init/lean/environment.lean index 4ffd2c23b7..6e5d7e077a 100644 --- a/library/init/lean/environment.lean +++ b/library/init/lean/environment.lean @@ -111,7 +111,7 @@ unsafe def setStateUnsafe {σ : Type} (ext : EnvExtension σ) (env : Environment constant setState {σ : Type} (ext : EnvExtension σ) (env : Environment) (s : σ) : Environment := default _ unsafe def getStateUnsafe {σ : Type} (ext : EnvExtension σ) (env : Environment) : σ := -let s : EnvExtensionState := env.extensions.get ext.idx in +let s : EnvExtensionState := env.extensions.get ext.idx; @unsafeCast _ _ ⟨ext.initial⟩ s @[implementedBy getStateUnsafe] @@ -119,8 +119,8 @@ constant getState {σ : Type} (ext : EnvExtension σ) (env : Environment) : σ : @[inline] unsafe def modifyStateUnsafe {σ : Type} (ext : EnvExtension σ) (env : Environment) (f : σ → σ) : Environment := { extensions := env.extensions.modify ext.idx $ λ s, - let s : σ := (@unsafeCast _ _ ⟨ext.initial⟩ s) in - let s : σ := f s in + let s : σ := (@unsafeCast _ _ ⟨ext.initial⟩ s); + let s : σ := f s; unsafeCast s, .. env } @@ -212,7 +212,7 @@ def getModuleEntries {α σ : Type} (ext : PersistentEnvExtension α σ) (env : def addEntry {α σ : Type} (ext : PersistentEnvExtension α σ) (env : Environment) (a : α) : Environment := ext.toEnvExtension.modifyState env $ λ s, - let state := ext.addEntryFn s.state a in + let state := ext.addEntryFn s.state a; { state := state, .. s } def getState {α σ : Type} (ext : PersistentEnvExtension α σ) (env : Environment) : σ := @@ -374,9 +374,9 @@ do pExts ← persistentEnvExtensionsRef.get, let entries : Array (Name × Array EnvExtensionEntry) := pExts.size.fold (λ i result, - let state := (pExts.get i).getState env in - let exportEntriesFn := (pExts.get i).exportEntriesFn in - let extName := (pExts.get i).name in + let state := (pExts.get i).getState env; + let exportEntriesFn := (pExts.get i).exportEntriesFn; + let extName := (pExts.get i).name; result.push (extName, exportEntriesFn state)) Array.empty, bytes ← serializeModifications (modListExtension.getState env), @@ -410,7 +410,7 @@ partial def importModulesAux : List Name → (NameSet × Array ModuleData) → I private partial def getEntriesFor (mod : ModuleData) (extId : Name) : Nat → Array EnvExtensionState | i := if i < mod.entries.size then - let curr := mod.entries.get i in + let curr := mod.entries.get i; if curr.1 == extId then curr.2 else getEntriesFor (i+1) else Array.empty @@ -420,7 +420,7 @@ do pExtDescrs ← persistentEnvExtensionsRef.get, pure $ mods.iterate env $ λ _ mod env, pExtDescrs.iterate env $ λ _ extDescr env, - let entries := getEntriesFor mod extDescr.name 0 in + let entries := getEntriesFor mod extDescr.name 0; extDescr.toEnvExtension.modifyState env $ λ s, { importedEntries := s.importedEntries.push entries, .. s } diff --git a/library/init/lean/format.lean b/library/init/lean/format.lean index d5095a04c7..62bc533ec6 100644 --- a/library/init/lean/format.lean +++ b/library/init/lean/format.lean @@ -56,10 +56,12 @@ structure SpaceResult := @[inline] private def merge (w : Nat) (r₁ : SpaceResult) (r₂ : Thunk SpaceResult) : SpaceResult := if r₁.exceeded || r₁.found then r₁ -else let y := r₂.get in - if y.exceeded || y.found then y - else let newSpace := r₁.space + y.space in - { space := newSpace, exceeded := newSpace > w } +else + let y := r₂.get; + if y.exceeded || y.found then y + else + let newSpace := r₁.space + y.space; + { space := newSpace, exceeded := newSpace > w } def spaceUptoLine : Format → Nat → SpaceResult | nil w := {} @@ -81,7 +83,7 @@ partial def be : Nat → Nat → String → List (Nat × Format) → String | w k out ((i, text s)::z) := be w (k + s.length) (out ++ s) z | w k out ((i, line)::z) := be w i ((out ++ "\n").pushn ' ' i) z | w k out ((i, choice f₁ f₂)::z) := - let r := merge w (spaceUptoLine f₁ w) (spaceUptoLine' z w) in + let r := merge w (spaceUptoLine f₁ w) (spaceUptoLine' z w); if r.exceeded then be w k out ((i, f₂)::z) else be w k out ((i, f₁)::z) @[inline] def bracket (l : String) (f : Format) (r : String) : Format := diff --git a/library/init/lean/level.lean b/library/init/lean/level.lean index cadb424d69..f47e73cabe 100644 --- a/library/init/lean/level.lean +++ b/library/init/lean/level.lean @@ -57,7 +57,7 @@ def Level.toNat : Level → Option Nat def Level.toOffset : Level → Level × Nat | Level.zero := (Level.zero, 0) -| (Level.succ l) := let (l', k) := Level.toOffset l in (l', k+1) +| (Level.succ l) := let (l', k) := Level.toOffset l; (l', k+1) | l := (l, 0) def Level.instantiate (s : Name → Option Level) : Level → Level @@ -109,7 +109,7 @@ partial def Result.format : Result → Bool → Format | (Result.num k) _ := toString k | (Result.offset f 0) r := Result.format f r | (Result.offset f (k+1)) r := - let f' := Result.format f false in + let f' := Result.format f false; parenIfFalse (f' ++ "+" ++ fmt (k+1)) r | (Result.maxNode fs) r := parenIfFalse (Format.group $ "max" ++ formatLst (λ r, Result.format r false) fs) r | (Result.imaxNode fs) r := parenIfFalse (Format.group $ "imax" ++ formatLst (λ r, Result.format r false) fs) r diff --git a/library/init/lean/modifiers.lean b/library/init/lean/modifiers.lean index a1f0d8b697..6ebf2de085 100644 --- a/library/init/lean/modifiers.lean +++ b/library/init/lean/modifiers.lean @@ -51,14 +51,14 @@ def privateHeader : Name := `_private @[export lean.mk_private_prefix_core] def mkPrivatePrefix (env : Environment) : Environment × Name := -let idx := privateExt.getState env in -let p := Name.mkNumeral (privateHeader ++ env.mainModule) idx in -let env := privateExt.setState env (idx+1) in +let idx := privateExt.getState env; +let p := Name.mkNumeral (privateHeader ++ env.mainModule) idx; +let env := privateExt.setState env (idx+1); (env, p) @[export lean.mk_private_name_core] def mkPrivateName (env : Environment) (n : Name) : Environment × Name := -let (env, p) := mkPrivatePrefix env in +let (env, p) := mkPrivatePrefix env; (env, p ++ n) def isPrivateName : Name → Bool diff --git a/library/init/lean/name.lean b/library/init/lean/name.lean index cf11710d69..52363c40bf 100644 --- a/library/init/lean/name.lean +++ b/library/init/lean/name.lean @@ -211,5 +211,5 @@ end Lean open Lean def String.toName (s : String) : Name := -let ps := s.split "." in +let ps := s.split "."; ps.foldl (λ n p, Name.mkString n p.trim) Name.anonymous diff --git a/library/init/lean/parser/parser.lean b/library/init/lean/parser/parser.lean index b975692d03..7ed9cd7c5b 100644 --- a/library/init/lean/parser/parser.lean +++ b/library/init/lean/parser/parser.lean @@ -92,7 +92,7 @@ def toErrorMsg (ctx : ParserContext) (s : ParserState) : String := match s.errorMsg with | none := "" | some msg := - let pos := ctx.fileMap.toPosition s.pos in + let pos := ctx.fileMap.toPosition s.pos; ctx.filename ++ ":" ++ toString pos.line ++ ":" ++ toString pos.column ++ " " ++ msg def mkNode (s : ParserState) (k : SyntaxNodeKind) (iniStackSz : Nat) : ParserState := @@ -102,9 +102,9 @@ match s with -- If there is an error but there are no new nodes on the stack, we just return `d` s else - let newNode := Syntax.node k (stack.extract iniStackSz stack.size) [] in - let stack := stack.shrink iniStackSz in - let stack := stack.push newNode in + let newNode := Syntax.node k (stack.extract iniStackSz stack.size) []; + let stack := stack.shrink iniStackSz; + let stack := stack.push newNode; ⟨stack, pos, cache, err⟩ def mkError (s : ParserState) (msg : String) : ParserState := @@ -188,7 +188,7 @@ abbrev TrailingParser := Parser trailing @[inline] def andthenAux (p q : BasicParserFn) : BasicParserFn := λ c s, - let s := p c s in + let s := p c s; if s.hasError then s else q c s @[inline] def andthenFn {k : ParserKind} (p q : ParserFn k) : ParserFn k := @@ -207,8 +207,8 @@ instance hashAndthen {k : ParserKind} : HasAndthen (Parser k) := @[inline] def nodeFn {k : ParserKind} (n : SyntaxNodeKind) (p : ParserFn k) : ParserFn k | a c s := - let iniSz := s.stackSize in - let s := p a c s in + let iniSz := s.stackSize; + let s := p a c s; s.mkNode n iniSz @[noinline] def nodeInfo (p : ParserInfo) : ParserInfo := @@ -227,9 +227,9 @@ node n p @[inline] def orelseFn {k : ParserKind} (p q : ParserFn k) : ParserFn k | a c s := - let iniSz := s.stackSize in - let iniPos := s.pos in - let s := p a c s in + let iniSz := s.stackSize; + let iniPos := s.pos; + let s := p a c s; if s.hasError && s.pos == iniPos then q a c (s.restore iniSz iniPos) else s @[noinline] def orelseInfo (p q : ParserInfo) : ParserInfo := @@ -248,8 +248,8 @@ instance hashOrelse {k : ParserKind} : HasOrelse (Parser k) := @[inline] def tryFn {k : ParserKind} (p : ParserFn k ) : ParserFn k | a c s := - let iniSz := s.stackSize in - let iniPos := s.pos in + let iniSz := s.stackSize; + let iniPos := s.pos; match p a c s with | ⟨stack, _, cache, some msg⟩ := ⟨stack.shrink iniSz, iniPos, cache, some msg⟩ | other := other @@ -260,10 +260,10 @@ instance hashOrelse {k : ParserKind} : HasOrelse (Parser k) := @[inline] def optionalFn {k : ParserKind} (p : ParserFn k) : ParserFn k := λ a c s, - let iniSz := s.stackSize in - let iniPos := s.pos in - let s := p a c s in - let s := if s.hasError then s.restore iniSz iniPos else s in + let iniSz := s.stackSize; + let iniPos := s.pos; + let s := p a c s; + let s := if s.hasError then s.restore iniSz iniPos else s; s.mkNode nullKind iniSz @[inline] def optional {k : ParserKind} (p : Parser k) : Parser k := @@ -272,17 +272,17 @@ instance hashOrelse {k : ParserKind} : HasOrelse (Parser k) := @[specialize] partial def manyAux {k : ParserKind} (p : ParserFn k) : ParserFn k | a c s := - let iniSz := s.stackSize in - let iniPos := s.pos in - let s := p a c s in + let iniSz := s.stackSize; + let iniPos := s.pos; + let s := p a c s; if s.hasError then s.restore iniSz iniPos else if iniPos == s.pos then s.mkError "invalid 'many' parser combinator application, parser did not consume anything" else manyAux a c s @[inline] def manyFn {k : ParserKind} (p : ParserFn k) : ParserFn k := λ a c s, - let iniSz := s.stackSize in - let s := manyAux p a c s in + let iniSz := s.stackSize; + let s := manyAux p a c s; s.mkNode nullKind iniSz @[inline] def many {k : ParserKind} (p : Parser k) : Parser k := @@ -294,35 +294,35 @@ andthen p (many p) @[specialize] private partial def sepByFnAux {k : ParserKind} (p : ParserFn k) (sep : ParserFn k) (allowTrailingSep : Bool) (iniSz : Nat) : Bool → ParserFn k | pOpt a c s := - let sz := s.stackSize in - let pos := s.pos in - let s := p a c s in + let sz := s.stackSize; + let pos := s.pos; + let s := p a c s; if s.hasError then if pOpt then - let s := s.restore sz pos in + let s := s.restore sz pos; s.mkNode nullKind iniSz else -- append `Syntax.missing` to make clear that List is incomplete - let s := s.pushSyntax Syntax.missing in + let s := s.pushSyntax Syntax.missing; s.mkNode nullKind iniSz else - let sz := s.stackSize in - let pos := s.pos in - let s := sep a c s in + let sz := s.stackSize; + let pos := s.pos; + let s := sep a c s; if s.hasError then - let s := s.restore sz pos in + let s := s.restore sz pos; s.mkNode nullKind iniSz else sepByFnAux allowTrailingSep a c s @[specialize] def sepByFn {k : ParserKind} (allowTrailingSep : Bool) (p : ParserFn k) (sep : ParserFn k) : ParserFn k | a c s := - let iniSz := s.stackSize in + let iniSz := s.stackSize; sepByFnAux p sep allowTrailingSep iniSz true a c s @[specialize] def sepBy1Fn {k : ParserKind} (allowTrailingSep : Bool) (p : ParserFn k) (sep : ParserFn k) : ParserFn k | a c s := - let iniSz := s.stackSize in + let iniSz := s.stackSize; sepByFnAux p sep allowTrailingSep iniSz false a c s @[noinline] def sepByInfo (p sep : ParserInfo) : ParserInfo := @@ -342,14 +342,14 @@ andthen p (many p) @[specialize] partial def satisfyFn (p : Char → Bool) (errorMsg : String := "unexpected character") : BasicParserFn | c s := - let i := s.pos in + let i := s.pos; if c.input.atEnd i then s.mkEOIError else if p (c.input.get i) then s.next c.input i else s.mkError errorMsg @[specialize] partial def takeUntilFn (p : Char → Bool) : BasicParserFn | c s := - let i := s.pos in + let i := s.pos; if c.input.atEnd i then s else if p (c.input.get i) then s else takeUntilFn c (s.next c.input i) @@ -362,16 +362,16 @@ andthenAux (satisfyFn p errorMsg) (takeWhileFn p) partial def finishCommentBlock : Nat → BasicParserFn | nesting c s := - let input := c.input in - let i := s.pos in + let input := c.input; + let i := s.pos; if input.atEnd i then s.mkEOIError else - let curr := input.get i in - let i := input.next i in + let curr := input.get i; + let i := input.next i; if curr == '-' then if input.atEnd i then s.mkEOIError else - let curr := input.get i in + let curr := input.get i; if curr == '/' then -- "-/" end of comment if nesting == 1 then s.next input i else finishCommentBlock (nesting-1) c (s.next input i) @@ -380,7 +380,7 @@ partial def finishCommentBlock : Nat → BasicParserFn else if curr == '/' then if input.atEnd i then s.mkEOIError else - let curr := input.get i in + let curr := input.get i; if curr == '-' then finishCommentBlock (nesting+1) c (s.next input i) else finishCommentBlock nesting c (s.setPos i) else finishCommentBlock nesting c (s.setPos i) @@ -388,23 +388,23 @@ partial def finishCommentBlock : Nat → BasicParserFn /- Consume whitespace and comments -/ partial def whitespace : BasicParserFn | c s := - let input := c.input in - let i := s.pos in + let input := c.input; + let i := s.pos; if input.atEnd i then s else - let curr := input.get i in + let curr := input.get i; if curr.isWhitespace then whitespace c (s.next input i) else if curr == '-' then - let i := input.next i in - let curr := input.get i in + let i := input.next i; + let curr := input.get i; if curr == '-' then andthenAux (takeUntilFn (= '\n')) whitespace c (s.next input i) else s else if curr == '/' then - let i := input.next i in - let curr := input.get i in + let i := input.next i; + let curr := input.get i; if curr == '-' then - let i := input.next i in - let curr := input.get i in + let i := input.next i; + let curr := input.get i; if curr == '-' then s -- "/--" doc comment is an actual token else andthenAux (finishCommentBlock 1) whitespace c (s.next input i) else s @@ -415,46 +415,46 @@ def mkEmptySubstringAt (s : String) (p : Nat) : Substring := private def rawAux {k : ParserKind} (startPos : Nat) (trailingWs : Bool) : ParserFn k | a c s := - let input := c.input in - let stopPos := s.pos in - let leading := mkEmptySubstringAt input startPos in - let val := input.extract startPos stopPos in + let input := c.input; + let stopPos := s.pos; + let leading := mkEmptySubstringAt input startPos; + let val := input.extract startPos stopPos; if trailingWs then - let s := whitespace c s in - let stopPos' := s.pos in - let trailing := { Substring . str := input, startPos := stopPos, stopPos := stopPos' } in - let atom := Syntax.atom (some { leading := leading, pos := startPos, trailing := trailing }) val in + let s := whitespace c s; + let stopPos' := s.pos; + let trailing := { Substring . str := input, startPos := stopPos, stopPos := stopPos' }; + let atom := Syntax.atom (some { leading := leading, pos := startPos, trailing := trailing }) val; s.pushSyntax atom else - let trailing := mkEmptySubstringAt input stopPos in - let atom := Syntax.atom (some { leading := leading, pos := startPos, trailing := trailing }) val in + let trailing := mkEmptySubstringAt input stopPos; + let atom := Syntax.atom (some { leading := leading, pos := startPos, trailing := trailing }) val; s.pushSyntax atom /-- Match an arbitrary Parser and return the consumed String in a `Syntax.atom`. -/ @[inline] def rawFn {k : ParserKind} (p : ParserFn k) (trailingWs := false) : ParserFn k | a c s := - let startPos := s.pos in - let s := p a c s in + let startPos := s.pos; + let s := p a c s; if s.hasError then s else rawAux startPos trailingWs a c s def hexDigitFn : BasicParserFn | c s := - let input := c.input in - let i := s.pos in + let input := c.input; + let i := s.pos; if input.atEnd i then s.mkEOIError else - let curr := input.get i in - let i := input.next i in + let curr := input.get i; + let i := input.next i; if curr.isDigit || ('a' <= curr && curr <= 'f') || ('A' <= curr && curr <= 'F') then s.setPos i else s.mkError "invalid hexadecimal numeral, hexadecimal digit expected" def quotedCharFn : BasicParserFn | c s := - let input := c.input in - let i := s.pos in + let input := c.input; + let i := s.pos; if input.atEnd i then s.mkEOIError else - let curr := input.get i in + let curr := input.get i; if curr == '\\' || curr == '\"' || curr == '\'' || curr == '\n' || curr == '\t' then s.next input i else if curr == 'x' then @@ -467,24 +467,24 @@ def quotedCharFn : BasicParserFn /-- Push `(Syntax.node tk )` into syntax stack -/ def mkNodeToken (n : SyntaxNodeKind) (startPos : Nat) : BasicParserFn := λ c s, -let input := c.input in -let stopPos := s.pos in -let leading := mkEmptySubstringAt input startPos in -let val := input.extract startPos stopPos in -let s := whitespace c s in -let wsStopPos := s.pos in -let trailing := { Substring . str := input, startPos := stopPos, stopPos := wsStopPos } in -let info := { SourceInfo . leading := leading, pos := startPos, trailing := trailing } in +let input := c.input; +let stopPos := s.pos; +let leading := mkEmptySubstringAt input startPos; +let val := input.extract startPos stopPos; +let s := whitespace c s; +let wsStopPos := s.pos; +let trailing := { Substring . str := input, startPos := stopPos, stopPos := wsStopPos }; +let info := { SourceInfo . leading := leading, pos := startPos, trailing := trailing }; s.pushSyntax (mkLit n val (some info)) partial def strLitFnAux (startPos : Nat) : BasicParserFn | c s := - let input := c.input in - let i := s.pos in + let input := c.input; + let i := s.pos; if input.atEnd i then s.mkEOIError else - let curr := input.get i in - let s := s.setPos (input.next i) in + let curr := input.get i; + let s := s.setPos (input.next i); if curr == '\"' then mkNodeToken strLitKind startPos c s else if curr == '\\' then andthenAux quotedCharFn strLitFnAux c s @@ -492,48 +492,46 @@ partial def strLitFnAux (startPos : Nat) : BasicParserFn def decimalNumberFn (startPos : Nat) : BasicParserFn := λ c s, - let s := takeWhileFn (λ c, c.isDigit) c s in - let input := c.input in - let i := s.pos in - let curr := input.get i in + let s := takeWhileFn (λ c, c.isDigit) c s; + let input := c.input; + let i := s.pos; + let curr := input.get i; let s := /- TODO(Leo): should we use a different kind for numerals containing decimal points? -/ if curr == '.' then - let i := input.next i in - let curr := input.get i in + let i := input.next i; + let curr := input.get i; if curr.isDigit then takeWhileFn (λ c, c.isDigit) c (s.setPos i) - else - s - else - s in + else s + else s; mkNodeToken numLitKind startPos c s def binNumberFn (startPos : Nat) : BasicParserFn := λ c s, - let s := takeWhile1Fn (λ c, c == '0' || c == '1') "expected binary number" c s in + let s := takeWhile1Fn (λ c, c == '0' || c == '1') "expected binary number" c s; mkNodeToken numLitKind startPos c s def octalNumberFn (startPos : Nat) : BasicParserFn := λ c s, - let s := takeWhile1Fn (λ c, '0' ≤ c && c ≤ '7') "expected octal number" c s in + let s := takeWhile1Fn (λ c, '0' ≤ c && c ≤ '7') "expected octal number" c s; mkNodeToken numLitKind startPos c s def hexNumberFn (startPos : Nat) : BasicParserFn := λ c s, - let s := takeWhile1Fn (λ c, ('0' ≤ c && c ≤ '9') || ('a' ≤ c && c ≤ 'f') || ('A' ≤ c && c ≤ 'F')) "expected hexadecimal number" c s in + let s := takeWhile1Fn (λ c, ('0' ≤ c && c ≤ '9') || ('a' ≤ c && c ≤ 'f') || ('A' ≤ c && c ≤ 'F')) "expected hexadecimal number" c s; mkNodeToken numLitKind startPos c s def numberFnAux : BasicParserFn := λ c s, - let input := c.input in - let startPos := s.pos in + let input := c.input; + let startPos := s.pos; if input.atEnd startPos then s.mkEOIError else - let curr := input.get startPos in + let curr := input.get startPos; if curr == '0' then - let i := input.next startPos in - let curr := input.get i in + let i := input.next startPos; + let curr := input.get i; if curr == 'b' || curr == 'B' then binNumberFn startPos c (s.next input i) else if curr == 'o' || curr == 'O' then @@ -549,14 +547,14 @@ def numberFnAux : BasicParserFn := def isIdCont : String → ParserState → Bool | input s := - let i := s.pos in - let curr := input.get i in + let i := s.pos; + let curr := input.get i; if curr == '.' then - let i := input.next i in + let i := input.next i; if input.atEnd i then false else - let curr := input.get i in + let curr := input.get i; isIdFirst curr || isIdBeginEscape curr else false @@ -574,57 +572,57 @@ def mkTokenAndFixPos (startPos : Nat) (tk : Option TokenConfig) : BasicParserFn match tk with | none := s.mkErrorAt "token expected" startPos | some tk := - let input := c.input in - let leading := mkEmptySubstringAt input startPos in - let val := tk.val in - let stopPos := startPos + val.bsize in - let s := s.setPos stopPos in - let s := whitespace c s in - let wsStopPos := s.pos in - let trailing := { Substring . str := input, startPos := stopPos, stopPos := wsStopPos } in - let atom := Syntax.atom (some { leading := leading, pos := startPos, trailing := trailing }) val in + let input := c.input; + let leading := mkEmptySubstringAt input startPos; + let val := tk.val; + let stopPos := startPos + val.bsize; + let s := s.setPos stopPos; + let s := whitespace c s; + let wsStopPos := s.pos; + let trailing := { Substring . str := input, startPos := stopPos, stopPos := wsStopPos }; + let atom := Syntax.atom (some { leading := leading, pos := startPos, trailing := trailing }) val; s.pushSyntax atom def mkIdResult (startPos : Nat) (tk : Option TokenConfig) (val : Name) : BasicParserFn := λ c s, -let stopPos := s.pos in +let stopPos := s.pos; if isToken startPos stopPos tk then mkTokenAndFixPos startPos tk c s else - let input := c.input in - let rawVal := { Substring . str := input, startPos := startPos, stopPos := stopPos } in - let s := whitespace c s in - let trailingStopPos := s.pos in - let leading := mkEmptySubstringAt input startPos in - let trailing := { Substring . str := input, startPos := stopPos, stopPos := trailingStopPos } in - let info := { SourceInfo . leading := leading, trailing := trailing, pos := startPos } in - let atom := Syntax.ident (some info) rawVal val [] [] in + let input := c.input; + let rawVal := { Substring . str := input, startPos := startPos, stopPos := stopPos }; + let s := whitespace c s; + let trailingStopPos := s.pos; + let leading := mkEmptySubstringAt input startPos; + let trailing := { Substring . str := input, startPos := stopPos, stopPos := trailingStopPos }; + let info := { SourceInfo . leading := leading, trailing := trailing, pos := startPos }; + let atom := Syntax.ident (some info) rawVal val [] []; s.pushSyntax atom partial def identFnAux (startPos : Nat) (tk : Option TokenConfig) : Name → BasicParserFn | r c s := - let input := c.input in - let i := s.pos in + let input := c.input; + let i := s.pos; if input.atEnd i then s.mkEOIError else - let curr := input.get i in + let curr := input.get i; if isIdBeginEscape curr then - let startPart := input.next i in - let s := takeUntilFn isIdEndEscape c (s.setPos startPart) in - let stopPart := s.pos in - let s := satisfyFn isIdEndEscape "end of escaped identifier expected" c s in + let startPart := input.next i; + let s := takeUntilFn isIdEndEscape c (s.setPos startPart); + let stopPart := s.pos; + let s := satisfyFn isIdEndEscape "end of escaped identifier expected" c s; if s.hasError then s else - let r := Name.mkString r (input.extract startPart stopPart) in + let r := Name.mkString r (input.extract startPart stopPart); if isIdCont input s then identFnAux r c s else mkIdResult startPos tk r c s else if isIdFirst curr then - let startPart := i in - let s := takeWhileFn isIdRest c (s.next input i) in - let stopPart := s.pos in - let r := Name.mkString r (input.extract startPart stopPart) in + let startPart := i; + let s := takeWhileFn isIdRest c (s.next input i); + let stopPart := s.pos; + let r := Name.mkString r (input.extract startPart stopPart); if isIdCont input s then identFnAux r c s else @@ -634,15 +632,15 @@ partial def identFnAux (startPos : Nat) (tk : Option TokenConfig) : Name → Bas private def tokenFnAux : BasicParserFn | c s := - let input := c.input in - let i := s.pos in - let curr := input.get i in + let input := c.input; + let i := s.pos; + let curr := input.get i; if curr == '\"' then strLitFnAux i c (s.next input i) else if curr.isDigit then numberFnAux c s else - let (_, tk) := c.tokens.matchPrefix input i in + let (_, tk) := c.tokens.matchPrefix input i; identFnAux i tk Name.anonymous c s private def updateCache (startPos : Nat) (s : ParserState) : ParserState := @@ -650,37 +648,37 @@ match s with | ⟨stack, pos, cache, none⟩ := if stack.size == 0 then s else - let tk := stack.back in + let tk := stack.back; ⟨stack, pos, { tokenCache := { startPos := startPos, stopPos := pos, token := tk } }, none⟩ | other := other def tokenFn : BasicParserFn := λ c s, - let input := c.input in - let i := s.pos in + let input := c.input; + let i := s.pos; if input.atEnd i then s.mkEOIError else - let tkc := s.cache.tokenCache in + let tkc := s.cache.tokenCache; if tkc.startPos == i then - let s := s.pushSyntax tkc.token in + let s := s.pushSyntax tkc.token; s.setPos tkc.stopPos else - let s := tokenFnAux c s in + let s := tokenFnAux c s; updateCache i s def peekToken (c : ParserContext) (s : ParserState) : ParserState × Option Syntax := -let iniSz := s.stackSize in -let iniPos := s.pos in -let s := tokenFn c s in +let iniSz := s.stackSize; +let iniPos := s.pos; +let s := tokenFn c s; if s.hasError then (s.restore iniSz iniPos, none) else - let stx := s.stxStack.back in + let stx := s.stxStack.back; (s.restore iniSz iniPos, some stx) @[inline] def satisfySymbolFn (p : String → Bool) (errorMsg : String) : BasicParserFn := λ c s, - let startPos := s.pos in - let s := tokenFn c s in + let startPos := s.pos; + let s := tokenFn c s; if s.hasError then s.mkErrorAt errorMsg startPos else @@ -730,7 +728,7 @@ def mkAtomicInfo (k : String) : ParserInfo := def numLitFn {k : ParserKind} : ParserFn k := λ _ c s, - let s := tokenFn c s in + let s := tokenFn c s; if s.hasError || !(s.stxStack.back.isOfKind numLitKind) then s.mkError "expected numeral" else s @[inline] def numLit {k : ParserKind} : Parser k := @@ -739,7 +737,7 @@ def numLitFn {k : ParserKind} : ParserFn k := def strLitFn {k : ParserKind} : ParserFn k := λ _ c s, -let s := tokenFn c s in +let s := tokenFn c s; if s.hasError || !(s.stxStack.back.isOfKind strLitKind) then s.mkError "expected string literal" else s @[inline] def strLit {k : ParserKind} : Parser k := @@ -748,7 +746,7 @@ if s.hasError || !(s.stxStack.back.isOfKind strLitKind) then s.mkError "expected def identFn {k : ParserKind} : ParserFn k := λ _ c s, -let s := tokenFn c s in +let s := tokenFn c s; if s.hasError || !(s.stxStack.back.isIdent) then s.mkError "expected identifier" else @@ -783,31 +781,31 @@ match s with else if stack.size == startSize + 1 then s else -- parser created more than one node, combine them into a single node - let node := Syntax.node nullKind (stack.extract startSize stack.size) [] in - let stack := stack.shrink startSize in + let node := Syntax.node nullKind (stack.extract startSize stack.size) []; + let stack := stack.shrink startSize; ⟨stack.push node, pos, cache, none⟩ def keepLatest (s : ParserState) (startStackSize : Nat) : ParserState := match s with | ⟨stack, pos, cache, _⟩ := - let node := stack.back in - let stack := stack.shrink startStackSize in - let stack := stack.push node in + let node := stack.back; + let stack := stack.shrink startStackSize; + let stack := stack.push node; ⟨stack, pos, cache, none⟩ def replaceLongest (s : ParserState) (startStackSize : Nat) (prevStackSize : Nat) : ParserState := -let s := s.mkLongestNodeAlt prevStackSize in +let s := s.mkLongestNodeAlt prevStackSize; s.keepLatest startStackSize end ParserState def longestMatchStep {k : ParserKind} (startSize : Nat) (startPos : String.Pos) (p : ParserFn k) : ParserFn k := λ a c s, -let prevErrorMsg := s.errorMsg in -let prevStopPos := s.pos in -let prevSize := s.stackSize in -let s := s.restore prevSize startPos in -let s := p a c s in +let prevErrorMsg := s.errorMsg; +let prevStopPos := s.pos; +let prevSize := s.stackSize; +let s := s.restore prevSize startPos; +let s := p a c s; match prevErrorMsg, s.errorMsg with | none, none := -- both succeeded if s.pos > prevStopPos then s.replaceLongest startSize prevSize -- replace @@ -828,27 +826,27 @@ if !s.hasError && s.stackSize > startSize + 1 then s.mkNode choiceKind startSize def longestMatchFnAux {k : ParserKind} (startSize : Nat) (startPos : String.Pos) : List (Parser k) → ParserFn k | [] := λ _ _ s, longestMatchMkResult startSize s | (p::ps) := λ a c s, - let s := longestMatchStep startSize startPos p.fn a c s in + let s := longestMatchStep startSize startPos p.fn a c s; longestMatchFnAux ps a c s def longestMatchFn₁ {k : ParserKind} (p : ParserFn k) : ParserFn k := λ a c s, -let startSize := s.stackSize in -let s := p a c s in +let startSize := s.stackSize; +let s := p a c s; if s.hasError then s else s.mkLongestNodeAlt startSize def longestMatchFn {k : ParserKind} : List (Parser k) → ParserFn k | [] := λ _ _ s, s.mkError "longestMatch: empty list" | [p] := longestMatchFn₁ p.fn | (p::ps) := λ a c s, - let startSize := s.stackSize in - let startPos := s.pos in - let s := p.fn a c s in + let startSize := s.stackSize; + let startPos := s.pos; + let s := p.fn a c s; if s.hasError then - let s := s.shrinkStack startSize in + let s := s.shrinkStack startSize; longestMatchFnAux startSize startPos ps a c s else - let s := s.mkLongestNodeAlt startSize in + let s := s.mkLongestNodeAlt startSize; longestMatchFnAux startSize startPos ps a c s def anyOfFn {k : ParserKind} : List (Parser k) → ParserFn k @@ -879,7 +877,7 @@ structure ParsingTables := (tokens : Trie TokenConfig := {}) def currLbp (c : ParserContext) (s : ParserState) : ParserState × Nat := -let (s, stx) := peekToken c s in +let (s, stx) := peekToken c s; match stx with | some (Syntax.atom _ sym) := match c.tokens.matchPrefix sym 0 with @@ -890,11 +888,11 @@ match stx with | _ := (s, 0) def indexed {α : Type} (map : TokenMap α) (c : ParserContext) (s : ParserState) : ParserState × List α := -let (s, stx) := peekToken c s in +let (s, stx) := peekToken c s; let find (n : Name) : ParserState × List α := match map.find n with | some as := (s, as) - | _ := (s, []) in + | _ := (s, []); match stx with | some (Syntax.atom _ sym) := find (mkSimpleName sym) | some (Syntax.ident _ _ _ _ _) := find `ident @@ -907,43 +905,43 @@ else s.mkNode nullKind iniSz -- throw error instead? def leadingParser (kind : String) (tables : ParsingTables) : ParserFn leading := λ a c s, - let iniSz := s.stackSize in - let (s, ps) := indexed tables.leadingTable c s in + let iniSz := s.stackSize; + let (s, ps) := indexed tables.leadingTable c s; if ps.isEmpty then s.mkError ("expected " ++ kind) else - let s := longestMatchFn ps a c s in + let s := longestMatchFn ps a c s; mkResult s iniSz def trailingParser (kind : String) (tables : ParsingTables) : ParserFn trailing := λ a c s, - let iniSz := s.stackSize in - let (s, ps) := indexed tables.trailingTable c s in + let iniSz := s.stackSize; + let (s, ps) := indexed tables.trailingTable c s; if ps.isEmpty then s.mkError ("expected trail of " ++ kind) -- better error message? else - let s := orelseFn (longestMatchFn ps) (anyOfFn tables.trailingParsers) a c s in + let s := orelseFn (longestMatchFn ps) (anyOfFn tables.trailingParsers) a c s; mkResult s iniSz partial def trailingLoop (kind : String) (tables : ParsingTables) (rbp : Nat) (c : ParserContext) : Syntax → ParserState → ParserState | left s := - let (s, lbp) := currLbp c s in + let (s, lbp) := currLbp c s; if rbp ≥ lbp then s.pushSyntax left else - let s := trailingParser kind tables left c s in + let s := trailingParser kind tables left c s; if s.hasError then s else - let left := s.stxStack.back in - let s := s.popSyntax in + let left := s.stxStack.back; + let s := s.popSyntax; trailingLoop left s def prattParser (kind : String) (tables : ParsingTables) : ParserFn leading := λ rbp c s, - let s := leadingParser kind tables rbp c s in + let s := leadingParser kind tables rbp c s; if s.hasError then s else - let left := s.stxStack.back in - let s := s.popSyntax in + let left := s.stxStack.back; + let s := s.popSyntax; trailingLoop kind tables rbp c left s def mkParserContext (env : Environment) (input : String) (filename : String) (tokens : Trie TokenConfig) : ParserContext := @@ -957,9 +955,9 @@ def mkParserState (input : String) : ParserState := { cache := initCacheForInput input } def runParser (env : Environment) (tables : ParsingTables) (input : String) (fileName := "") (kind := "
") : Except String Syntax := -let c := mkParserContext env input fileName tables.tokens in -let s := mkParserState input in -let s := prattParser kind tables (0 : Nat) c s in +let c := mkParserContext env input fileName tables.tokens; +let s := mkParserState input; +let s := prattParser kind tables (0 : Nat) c s; if s.hasError then Except.error (s.toErrorMsg c) else @@ -979,7 +977,7 @@ do tables ← tablesRef.get, tables ← updateTokens tables p.info, match p.info.firstTokens with | FirstTokens.tokens tks := - let tables := tks.foldl (λ (tables : ParsingTables) tk, { leadingTable := tables.leadingTable.insert (mkSimpleName tk.val) p, .. tables }) tables in + let tables := tks.foldl (λ (tables : ParsingTables) tk, { leadingTable := tables.leadingTable.insert (mkSimpleName tk.val) p, .. tables }) tables; tablesRef.set tables | _ := throw (IO.userError ("invalid builtin parser '" ++ toString declName ++ "', initial token is not statically known")) @@ -990,17 +988,17 @@ do tables ← tablesRef.get, tables ← updateTokens tables p.info, match p.info.firstTokens with | FirstTokens.tokens tks := - let tables := tks.foldl (λ (tables : ParsingTables) tk, { trailingTable := tables.trailingTable.insert (mkSimpleName tk.val) p, .. tables }) tables in + let tables := tks.foldl (λ (tables : ParsingTables) tk, { trailingTable := tables.trailingTable.insert (mkSimpleName tk.val) p, .. tables }) tables; tablesRef.set tables | _ := - let tables := { trailingParsers := p :: tables.trailingParsers, .. tables } in + let tables := { trailingParsers := p :: tables.trailingParsers, .. tables }; tablesRef.set tables def declareBuiltinParser (env : Environment) (addFnName : Name) (refDeclName : Name) (declName : Name) : IO Environment := -let name := `_regBuiltinParser ++ declName in -let type := Expr.app (mkConst `IO) (mkConst `Unit) in -let val := mkCApp addFnName [mkConst refDeclName, toExpr declName, mkConst declName] in -let decl := Declaration.defnDecl { name := name, lparams := [], type := type, value := val, hints := ReducibilityHints.opaque, isUnsafe := false } in +let name := `_regBuiltinParser ++ declName; +let type := Expr.app (mkConst `IO) (mkConst `Unit); +let val := mkCApp addFnName [mkConst refDeclName, toExpr declName, mkConst declName]; +let decl := Declaration.defnDecl { name := name, lparams := [], type := type, value := val, hints := ReducibilityHints.opaque, isUnsafe := false }; match env.addAndCompile {} decl with | none := throw (IO.userError ("failed to emit registration code for builtin parser '" ++ toString declName ++ "'")) | some env := IO.ofExcept (setInitAttr env name) diff --git a/library/init/lean/parser/trie.lean b/library/init/lean/parser/trie.lean index 5c1325e3f0..c68e72b682 100644 --- a/library/init/lean/parser/trie.lean +++ b/library/init/lean/parser/trie.lean @@ -31,8 +31,8 @@ private partial def insertEmptyAux (s : String) (val : α) : String.Pos → Trie | i := match s.atEnd i with | true := Trie.Node (some val) RBNode.leaf | false := - let c := s.get i in - let t := insertEmptyAux (s.next i) in + let c := s.get i; + let t := insertEmptyAux (s.next i); Trie.Node none (RBNode.singleton c t) private partial def insertAux (s : String) (val : α) : Trie α → String.Pos → Trie α @@ -40,11 +40,11 @@ private partial def insertAux (s : String) (val : α) : Trie α → String.Pos match s.atEnd i with | true := Trie.Node (some val) m -- overrides old value | false := - let c := s.get i in - let i := s.next i in + let c := s.get i; + let i := s.next i; let t := match RBNode.find Char.lt m c with | none := insertEmptyAux s val i - | some t := insertAux t i in + | some t := insertAux t i; Trie.Node v (RBNode.insert Char.lt m c t) def insert (t : Trie α) (s : String) (val : α) : Trie α := @@ -55,8 +55,8 @@ private partial def findAux (s : String) : Trie α → String.Pos → Option α match s.atEnd i with | true := val | false := - let c := s.get i in - let i := s.next i in + let c := s.get i; + let i := s.next i; match RBNode.find Char.lt m c with | none := none | some t := findAux t i @@ -74,9 +74,9 @@ private partial def matchPrefixAux (s : String) : Trie α → String.Pos → (St match s.atEnd i with | true := updtAcc v i acc | false := - let acc := updtAcc v i acc in - let c := s.get i in - let i := s.next i in + let acc := updtAcc v i acc; + let c := s.get i; + let i := s.next i; match RBNode.find Char.lt m c with | some t := matchPrefixAux t i acc | none := acc diff --git a/library/init/lean/position.lean b/library/init/lean/position.lean index 324cfef4bd..d4be3e991c 100644 --- a/library/init/lean/position.lean +++ b/library/init/lean/position.lean @@ -43,8 +43,8 @@ private partial def ofStringAux (s : String) : String.Pos → Nat → Array Stri | i line ps lines := if s.atEnd i then { source := s, positions := ps.push i, lines := lines.push line } else - let c := s.get i in - let i := s.next i in + let c := s.get i; + let i := s.next i; if c == '\n' then ofStringAux i (line+1) (ps.push i) (lines.push (line+1)) else ofStringAux i line ps lines @@ -59,11 +59,11 @@ private partial def toColumnAux (str : String) (lineBeginPos : String.Pos) (pos /- Remark: `pos` is in `[ps.get b, ps.get e]` and `b < e` -/ private partial def toPositionAux (str : String) (ps : Array Nat) (lines : Array Nat) (pos : String.Pos) : Nat → Nat → Position | b e := - let posB := ps.get b in + let posB := ps.get b; if e == b + 1 then { line := lines.get b, column := toColumnAux str posB pos posB 0 } else - let m := (b + e) / 2 in - let posM := ps.get m in + let m := (b + e) / 2; + let posM := ps.get m; if pos == posM then { line := lines.get m, column := 0 } else if pos > posM then toPositionAux m e else toPositionAux b m diff --git a/library/init/lean/syntax.lean b/library/init/lean/syntax.lean index a8bca14864..59b1bf7d5f 100644 --- a/library/init/lean/syntax.lean +++ b/library/init/lean/syntax.lean @@ -157,9 +157,9 @@ partial def updateTrailing (trailing : Substring) : Syntax → Syntax | n@(Syntax.node k args scopes) := if args.size == 0 then n else - let i := args.size - 1 in - let last := updateTrailing (args.get i) in - let args := args.set i last in + let i := args.size - 1; + let last := updateTrailing (args.get i); + let args := args.set i last; Syntax.node k args scopes | other := other @@ -194,15 +194,15 @@ open Lean.Format protected partial def formatStx : Syntax → Format | (atom info val) := format $ repr val | (ident _ _ val pre scopes) := - let scopes := pre.map format ++ scopes.reverse.map format in - let scopes := match scopes with [] := format "" | _ := bracket "{" (joinSep scopes ", ") "}" in + let scopes := pre.map format ++ scopes.reverse.map format; + let scopes := match scopes with [] := format "" | _ := bracket "{" (joinSep scopes ", ") "}"; format "`" ++ format val ++ scopes | (node kind args scopes) := - let scopes := match scopes with [] := format "" | _ := bracket "{" (joinSep scopes.reverse ", ") "}" in + let scopes := match scopes with [] := format "" | _ := bracket "{" (joinSep scopes.reverse ", ") "}"; if kind = `Lean.Parser.noKind then sbracket $ scopes ++ joinSep (args.toList.map formatStx) line else - let shorterName := kind.replacePrefix `Lean.Parser Name.anonymous in + let shorterName := kind.replacePrefix `Lean.Parser Name.anonymous; paren $ joinSep ((format shorterName ++ scopes) :: args.toList.map formatStx) line | missing := "" @@ -228,7 +228,7 @@ Syntax.node nullKind args [] /- Helper functions for creating string and numeric literals -/ def mkLit (kind : SyntaxNodeKind) (val : String) (info : Option SourceInfo := none) : Syntax := -let atom := Syntax.atom info val in +let atom := Syntax.atom info val; Syntax.node kind (Array.singleton atom) [] def mkStrLit (val : String) (info : Option SourceInfo := none) : Syntax := @@ -268,7 +268,7 @@ private partial def decodeBinLitAux (s : String) : Nat → Nat → Option Nat | i val := if s.atEnd i then some val else - let c := s.get i in + let c := s.get i; if c == '0' then decodeBinLitAux (s.next i) (2*val) else if c == '1' then decodeBinLitAux (s.next i) (2*val + 1) else none @@ -277,7 +277,7 @@ private partial def decodeOctalLitAux (s : String) : Nat → Nat → Option Nat | i val := if s.atEnd i then some val else - let c := s.get i in + let c := s.get i; if '0' ≤ c && c ≤ '7' then decodeOctalLitAux (s.next i) (8*val + c.toNat - '0'.toNat) else none @@ -285,7 +285,7 @@ private partial def decodeHexLitAux (s : String) : Nat → Nat → Option Nat | i val := if s.atEnd i then some val else - let c := s.get i in + let c := s.get i; if '0' ≤ c && c ≤ '9' then decodeHexLitAux (s.next i) (16*val + c.toNat - '0'.toNat) else if 'a' ≤ c && c ≤ 'f' then decodeHexLitAux (s.next i) (16*val + 10 + c.toNat - 'a'.toNat) else if 'A' ≤ c && c ≤ 'F' then decodeHexLitAux (s.next i) (16*val + 10 + c.toNat - 'A'.toNat) @@ -295,24 +295,24 @@ private partial def decodeDecimalLitAux (s : String) : Nat → Nat → Option Na | i val := if s.atEnd i then some val else - let c := s.get i in + let c := s.get i; if '0' ≤ c && c ≤ '9' then decodeDecimalLitAux (s.next i) (10*val + c.toNat - '0'.toNat) else none private def decodeNatLitVal (s : String) : Option Nat := -let len := s.length in +let len := s.length; if len == 0 then none else - let c := s.get 0 in + let c := s.get 0; if c == '0' then if len == 1 then some 0 else - let c := s.get 1 in - if c == 'x' || c == 'X' then decodeHexLitAux s 2 0 - else if c == 'b' || c == 'B' then decodeBinLitAux s 2 0 - else if c == 'o' || c == 'O' then decodeOctalLitAux s 2 0 - else if c.isDigit then decodeDecimalLitAux s 0 0 - else none + let c := s.get 1; + if c == 'x' || c == 'X' then decodeHexLitAux s 2 0 + else if c == 'b' || c == 'B' then decodeBinLitAux s 2 0 + else if c == 'o' || c == 'O' then decodeOctalLitAux s 2 0 + else if c.isDigit then decodeDecimalLitAux s 0 0 + else none else if c.isDigit then decodeDecimalLitAux s 0 0 else none diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp index c1a66ccf53..00808fe036 100644 --- a/src/frontends/lean/builtin_exprs.cpp +++ b/src/frontends/lean/builtin_exprs.cpp @@ -104,14 +104,11 @@ static expr parse_let_body(parser & p, pos_info const & pos, bool in_do_block) { } } } else { - if (p.curr_is_token(get_comma_tk())) { - p.next(); - return parse_let(p, pos, in_do_block); - } else if (p.curr_is_token(get_in_tk())) { + if (p.curr_is_token(get_in_tk()) || p.curr_is_token(get_semicolon_tk())) { p.next(); return p.parse_expr(); } else { - p.maybe_throw_error({"invalid let declaration, 'in' or ',' expected", p.pos()}); + p.maybe_throw_error({"invalid let declaration, 'in' or ';' expected", p.pos()}); return p.parse_expr(); } }