feat: peek?, shrink, shouldBeEOI

Author: Qiu233

Binary/Basic.lean

@@ -97,15 +97,15 @@ instance : MonadFinally Get where
       match s with
       | .success a k =>
         let r := f (some a) k
-        let rec go' r :=
+        let rec @[specialize] go' r :=
           match r with
           | .success b k' => .success (a, b) k'
           | .error err k' => .error err k'
           | .pending fn => .pending fun bytes => go' <| fn bytes
         go' r
       | .error err _ =>
         let r := f none d -- backtracking
-        let rec go'' r :=
+        let rec @[specialize] go'' r :=
           match r with
           | .success _ k' => .error err k' -- caught, we ignore the inner error
           | .error err' k' => .error err' k' -- the finalizer throws an error
@@ -123,6 +123,18 @@ protected def DecodeResult.mkEOI : Decoder → DecodeResult α := .error .eoi
 @[always_inline]
 def throwEOI : Get α := DecodeResult.mkEOI
 
+/-- Drop the parsed data from inner buffer. This can be used to save memory. -/
+@[always_inline]
+def shrink : Get Unit := fun d =>
+  DecodeResult.success () { data := d.data.extract d.offset d.data.size, offset := 0 }
+
+@[always_inline]
+def peek? : Get (Option UInt8) := fun d =>
+  if h : d.offset < d.data.size then
+    DecodeResult.success (some d.data[d.offset]) d
+  else
+    DecodeResult.success none d
+
 class Decode (α : Type) where
   get : Get α
 export Decode (get)

Binary/Get.lean

@@ -7,6 +7,10 @@ namespace Binary
 
 public section
 
+@[always_inline]
+def fail (msg : String) : Get α :=
+  throw (.userError msg)
+
 @[always_inline, specialize]
 def many (p : Get α) : Get (Array α) := do
   let mut data := #[]
@@ -21,6 +25,12 @@ def many1 (p : Get α) : Get (Array α) := do
   let rest ← many p
   return rest.insertIdx 0 first
 
+@[always_inline, specialize]
+def shouldBeEOI : Get Unit := do
+  let x ← remaining
+  if x > 0 then
+    fail "expected EOI"
+
 -- TODO: refactor following definitions for performance
 
 @[inline, specialize]

Binary/UTF8/Get.lean

@@ -19,10 +19,6 @@ private def byteToChar (b : UInt8) : Char :=
 private def chars_to_string (xs : Array Char) : String :=
   String.ofList xs.toList
 
-@[always_inline]
-def fail {α} (msg : String) : Get α :=
-  throw (.userError msg)
-
 @[always_inline, specialize]
 def satisfy (p : Char → Bool) : Get Char := do
   let b ← getThe UInt8