feat: more functions in the bytearray parser and move .eof out
diff --git a/src/Lean/ErrorExplanation.lean b/src/Lean/ErrorExplanation.lean index 3a1e713..6941a81 100644 --- a/src/Lean/ErrorExplanation.lean +++ b/src/Lean/ErrorExplanation.lean
@@ -89,7 +89,7 @@ upToWs (nonempty : Bool) : Parser String := fun it => let it' := it.find fun c => c.isWhitespace if nonempty && it'.pos == it.pos then - .error it' "Expected a nonempty string" + .error it' (.other "Expected a nonempty string") else .success it' (it.extract it') @@ -176,7 +176,7 @@ private def ValidationM.run (p : ValidationM α) (input : String) : Except (Nat × String) α := match p (.ofSource input) with | .success _ res => Except.ok res - | .error s err => Except.error (s.getLineNumber, err) + | .error s err => Except.error (s.getLineNumber, toString err) /-- Matches `p` as many times as possible, followed by EOF. If `p` cannot be matched prior to the end @@ -286,7 +286,7 @@ labelingExampleErrors {α} (header : String) (x : ValidationM α) : ValidationM α := fun s => match x s with | res@(.success ..) => res - | .error s' msg => .error s' s!"Example '{header}' is malformed: {msg}" + | .error s' msg => .error s' (.other s!"Example '{header}' is malformed: {msg}") /-- If `line` is a level-`level` header and, if `title?` is non-`none`, its title is `title?`,
diff --git a/src/Std/Internal/Parsec/Basic.lean b/src/Std/Internal/Parsec/Basic.lean index e088a7f..ed10ed5 100644 --- a/src/Std/Internal/Parsec/Basic.lean +++ b/src/Std/Internal/Parsec/Basic.lean
@@ -1,24 +1,47 @@ /- Copyright (c) 2021 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Author: Dany Fabian, Henrik Böving +Author: Dany Fabian, Henrik Böving, Sofia Rodrigues -/ +module + prelude -import Init.NotationExtra -import Init.Data.ToString.Macro +public import Init.NotationExtra +public import Init.Data.ToString.Macro -namespace Std.Internal +public section +namespace Std +namespace Internal namespace Parsec +/-- +Error type for the `ParseResult`. It separates `eof` from the rest of the errors in order to +improve the error handling for this case in parsers that can receive incomplete data and then reparse it. +-/ +inductive Error where + | eof + | other (s : String) + deriving Repr + +instance : ToString Error where + toString + | .eof => "unexpected end of input" + | .other s => s + +/-- +The result of parsing some string. +-/ inductive ParseResult (α : Type) (ι : Type) where | success (pos : ι) (res : α) - | error (pos : ι) (err : String) + | error (pos : ι) (err : Error) deriving Repr end Parsec -def Parsec (ι : Type) (α : Type) : Type := ι → Parsec.ParseResult α ι +@[expose] +def Parsec (ι : Type) (α : Type) : Type := + ι → Parsec.ParseResult α ι namespace Parsec @@ -34,26 +57,21 @@ variable [DecidableEq idx] [DecidableEq elem] [Input ι elem idx] instance : Inhabited (Parsec ι α) where - default := fun it => .error it "" + default := fun it => ParseResult.error it (.other "") @[always_inline, inline] protected def pure (a : α) : Parsec ι α := fun it => .success it a @[always_inline, inline] -def bind {α β : Type} (f : Parsec ι α) (g : α → Parsec ι β) : Parsec ι β := fun it => +protected def bind {α β : Type} (f : Parsec ι α) (g : α → Parsec ι β) : Parsec ι β := fun it => match f it with | .success rem a => g a rem | .error pos msg => .error pos msg -@[always_inline] -instance : Monad (Parsec ι) where - pure := Parsec.pure - bind := Parsec.bind - @[always_inline, inline] def fail (msg : String) : Parsec ι α := fun it => - .error it msg + .error it (.other msg) @[inline] def tryCatch (p : Parsec ι α) (csuccess : α → Parsec ι β) (cerror : Unit → Parsec ι β) @@ -64,6 +82,11 @@ -- We assume that it.s never changes as the `Parsec` monad only modifies `it.pos`. if Input.pos it = Input.pos rem then cerror () rem else .error rem err +@[always_inline] +instance : Monad (Parsec ι) where + pure := Parsec.pure + bind := Parsec.bind + @[always_inline, inline] def orElse (p : Parsec ι α) (q : Unit → Parsec ι α) : Parsec ι α := tryCatch p pure q @@ -79,12 +102,10 @@ failure := fail "" orElse := orElse -def expectedEndOfInput := "expected end of input" - @[inline] def eof : Parsec ι Unit := fun it => if Input.hasNext it then - .error it expectedEndOfInput + .error it .eof else .success it () @@ -102,8 +123,9 @@ @[inline] def many1 (p : Parsec ι α) : Parsec ι <| Array α := do manyCore p #[← p] -def unexpectedEndOfInput := "unexpected end of input" - +/-- +Gets the next input element. +-/ @[inline] def any : Parsec ι elem := fun it => if h : Input.hasNext it then @@ -111,19 +133,28 @@ let it' := Input.next' it h .success it' c else - .error it unexpectedEndOfInput + .error it .eof +/-- +Checks if the next input element matches some condition. +-/ @[inline] def satisfy (p : elem → Bool) : Parsec ι elem := attempt do let c ← any if p c then return c else fail "condition not satisfied" +/-- +Fails if `p` succeeds, otherwise succeeds without consuming input. +-/ @[inline] def notFollowedBy (p : Parsec ι α) : Parsec ι Unit := fun it => match p it with - | .success _ _ => .error it "" + | .success _ _ => .error it (.other "") | .error _ _ => .success it () +/-- +Peeks at the next element, returns `some` if exists else `none`, does not consume input. +-/ @[inline] def peek? : Parsec ι (Option elem) := fun it => if h : Input.hasNext it then @@ -131,13 +162,32 @@ else .success it none +/-- +Peeks at the next element, returns `some elem` if it satisfies `p`, else `none`. Does not consume input. +-/ +@[inline] +def peekWhen? (p : elem → Bool) : Parsec ι (Option elem) := do + let some data ← peek? + | return none + + if p data then + return some data + else + return none + +/-- +Peeks at the next element, errors on EOF, does not consume input. +-/ @[inline] def peek! : Parsec ι elem := fun it => if h : Input.hasNext it then .success it (Input.curr' it h) else - .error it unexpectedEndOfInput + .error it .eof +/-- +Peeks at the next element or returns a default if at EOF, does not consume input. +-/ @[inline] def peekD (default : elem) : Parsec ι elem := fun it => if h : Input.hasNext it then @@ -145,23 +195,37 @@ else .success it default +/-- +Consumes one element if available, otherwise errors on EOF. +-/ @[inline] def skip : Parsec ι Unit := fun it => if h : Input.hasNext it then .success (Input.next' it h) () else - .error it unexpectedEndOfInput + .error it .eof +/-- +Parses zero or more chars with `p`, accumulates into a string. +-/ @[specialize] partial def manyCharsCore (p : Parsec ι Char) (acc : String) : Parsec ι String := tryCatch p (manyCharsCore p <| acc.push ·) (fun _ => pure acc) +/-- +Parses zero or more chars with `p` into a string. +-/ @[inline] -def manyChars (p : Parsec ι Char) : Parsec ι String := manyCharsCore p "" +def manyChars (p : Parsec ι Char) : Parsec ι String := do + manyCharsCore p "" +/-- +Parses one or more chars with `p` into a string, errors if none. +-/ @[inline] -def many1Chars (p : Parsec ι Char) : Parsec ι String := do manyCharsCore p (← p).toString +def many1Chars (p : Parsec ι Char) : Parsec ι String := do + manyCharsCore p (← p).toString end Parsec - -end Std.Internal +end Internal +end Std
diff --git a/src/Std/Internal/Parsec/ByteArray.lean b/src/Std/Internal/Parsec/ByteArray.lean index f3912b1..b246f4e 100644 --- a/src/Std/Internal/Parsec/ByteArray.lean +++ b/src/Std/Internal/Parsec/ByteArray.lean
@@ -3,12 +3,17 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Henrik Böving -/ -prelude -import Std.Internal.Parsec.Basic -import Init.Data.ByteArray.Basic -import Init.Data.String.Extra +module -namespace Std.Internal +prelude +public import Std.Internal.Parsec.Basic +public import Init.Data.ByteArray.Basic +public import Init.Data.String.Extra + +public section + +namespace Std +namespace Internal namespace Parsec namespace ByteArray @@ -22,27 +27,47 @@ abbrev Parser (α : Type) : Type := Parsec ByteArray.Iterator α +/-- +Run a `Parser` on a `ByteArray`, returns either the result or an error string with offset. +-/ protected def Parser.run (p : Parser α) (arr : ByteArray) : Except String α := match p arr.iter with | .success _ res => Except.ok res - | .error it err => Except.error s!"offset {repr it.pos}: {err}" + | .error it (.other err) => Except.error s!"offset {repr it.pos}: {err}" + | .error it .eof => Except.error s!"offset {repr it.pos}: end of file" +/-- +Parse a single byte equal to `b`, fails if different. +-/ @[inline] def pbyte (b : UInt8) : Parser UInt8 := attempt do if (← any) = b then pure b else fail s!"expected: '{b}'" +/-- +Skip a single byte equal to `b`, fails if different. +-/ @[inline] -def skipByte (b : UInt8) : Parser Unit := pbyte b *> pure () +def skipByte (b : UInt8) : Parser Unit := + pbyte b *> pure () +/-- +Skip a sequence of bytes equal to the given `ByteArray`. +-/ def skipBytes (arr : ByteArray) : Parser Unit := do for b in arr do skipByte b +/-- +Parse a string by matching its UTF-8 bytes, returns the string on success. +-/ @[inline] def pstring (s : String) : Parser String := do skipBytes s.toUTF8 return s +/-- +Skip a string by matching its UTF-8 bytes. +-/ @[inline] def skipString (s : String) : Parser Unit := pstring s *> pure () @@ -59,14 +84,24 @@ @[inline] def skipByteChar (c : Char) : Parser Unit := skipByte c.toUInt8 +/-- +Parse an ASCII digit `0-9` as a `Char`. +-/ @[inline] def digit : Parser Char := attempt do let b ← any if '0'.toUInt8 ≤ b ∧ b ≤ '9'.toUInt8 then return Char.ofUInt8 b else fail s!"digit expected" +/-- +Convert a byte representing `'0'..'9'` to a `Nat`. +-/ @[inline] -private def digitToNat (b : UInt8) : Nat := (b - '0'.toUInt8).toNat +private def digitToNat (b : UInt8) : Nat := + (b - '0'.toUInt8).toNat +/-- +Parse zero or more ASCII digits into a `Nat`, continuing until non-digit or EOF. +-/ @[inline] private partial def digitsCore (acc : Nat) : Parser Nat := fun it => /- @@ -88,11 +123,17 @@ else (acc, it) +/-- +Parse one or more ASCII digits into a `Nat`. +-/ @[inline] def digits : Parser Nat := do let d ← digit digitsCore (digitToNat d.toUInt8) +/-- +Parse a hex digit `0-9`, `a-f`, or `A-F` as a `Char`. +-/ @[inline] def hexDigit : Parser Char := attempt do let b ← any @@ -100,6 +141,20 @@ ∨ ('a'.toUInt8 ≤ b ∧ b ≤ 'f'.toUInt8) ∨ ('A'.toUInt8 ≤ b ∧ b ≤ 'F'.toUInt8) then return Char.ofUInt8 b else fail s!"hex digit expected" +/-- +Parse an octal digit `0-7` as a `Char`. +-/ +@[inline] +def octDigit : Parser Char := attempt do + let b ← any + if '0'.toUInt8 ≤ b ∧ b ≤ '7'.toUInt8 then + return Char.ofUInt8 b + else + fail s!"octal digit expected" + +/-- +Parse an ASCII letter `a-z` or `A-Z` as a `Char`. +-/ @[inline] def asciiLetter : Parser Char := attempt do let b ← any @@ -118,17 +173,65 @@ else it +/-- +Skip whitespace: tabs, newlines, carriage returns, and spaces. +-/ @[inline] def ws : Parser Unit := fun it => .success (skipWs it) () +/-- +Parse `n` bytes from the input into a `ByteArray`, errors if not enough bytes. +-/ def take (n : Nat) : Parser ByteArray := fun it => let subarr := it.array.extract it.idx (it.idx + n) if subarr.size != n then - .error it s!"expected: {n} bytes" + .error it .eof else .success (it.forward n) subarr +/-- +Parses while a predicate is satisfied. +-/ +@[inline] +partial def takeWhile (pred : UInt8 → Bool) : Parser ByteArray := + fun it => + let rec findEnd (count : Nat) (iter : ByteArray.Iterator) : (Nat × ByteArray.Iterator) := + if ¬iter.hasNext then (count, iter) + else if pred iter.curr then findEnd (count + 1) iter.next + else (count, iter) + + let (length, newIt) := findEnd 0 it + .success newIt (it.array.extract it.idx (it.idx + length)) + +/-- +Parses until a predicate is satisfied (exclusive). +-/ +@[inline] +def takeUntil (pred : UInt8 → Bool) : Parser ByteArray := + takeWhile (fun b => ¬pred b) + +/-- +Skips while a predicate is satisfied. +-/ +@[inline] +partial def skipWhile (pred : UInt8 → Bool) : Parser Unit := + fun it => + let rec findEnd (count : Nat) (iter : ByteArray.Iterator) : ByteArray.Iterator := + if ¬iter.hasNext then iter + else if pred iter.curr then findEnd (count + 1) iter.next + else iter + + .success (findEnd 0 it) () + +/-- +Skips until a predicate is satisfied. +-/ +@[inline] +def skipUntil (pred : UInt8 → Bool) : Parser Unit := + skipWhile (fun b => ¬pred b) + end ByteArray end Parsec -end Std.Internal +end Internal +end Std
diff --git a/src/Std/Internal/Parsec/String.lean b/src/Std/Internal/Parsec/String.lean index e543018..9ed86a9 100644 --- a/src/Std/Internal/Parsec/String.lean +++ b/src/Std/Internal/Parsec/String.lean
@@ -3,8 +3,12 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Dany Fabian, Henrik Böving -/ +module + prelude -import Std.Internal.Parsec.Basic +public import Std.Internal.Parsec.Basic + +public section namespace Std.Internal namespace Parsec @@ -20,34 +24,55 @@ abbrev Parser (α : Type) : Type := Parsec String.Iterator α +/-- +Run a `Parser` on a `String`, returns either the result or an error string with offset. +-/ protected def Parser.run (p : Parser α) (s : String) : Except String α := match p s.mkIterator with | .success _ res => Except.ok res - | .error it err => Except.error s!"offset {repr it.i.byteIdx}: {err}" + | .error it (.other err) => Except.error s!"offset {repr it.pos}: {err}" + | .error it .eof => Except.error s!"offset {repr it.pos}: end of file" -/-- Parses the given string. -/ +/-- +Parses the given string. +-/ def pstring (s : String) : Parser String := fun it => let substr := it.extract (it.forward s.length) if substr = s then .success (it.forward s.length) substr else - .error it s!"expected: {s}" + .error it (.other s!"expected: {s}") +/-- +Skips the given string. +-/ @[inline] def skipString (s : String) : Parser Unit := pstring s *> pure () +/-- +Parses the given char. +-/ @[inline] def pchar (c : Char) : Parser Char := attempt do if (← any) = c then pure c else fail s!"expected: '{c}'" +/-- +Skips the given char. +-/ @[inline] def skipChar (c : Char) : Parser Unit := pchar c *> pure () +/-- +Parse an ASCII digit `0-9` as a `Char`. +-/ @[inline] def digit : Parser Char := attempt do let c ← any if '0' ≤ c ∧ c ≤ '9' then return c else fail s!"digit expected" +/-- +Convert a byte representing `'0'..'9'` to a `Nat`. +-/ @[inline] private def digitToNat (b : Char) : Nat := b.toNat - '0'.toNat @@ -72,11 +97,17 @@ else (acc, it) +/-- +Parse one or more ASCII digits into a `Nat`. +-/ @[inline] def digits : Parser Nat := do let d ← digit digitsCore (digitToNat d) +/-- +Parse a hex digit `0-9`, `a-f`, or `A-F` as a `Char`. +-/ @[inline] def hexDigit : Parser Char := attempt do let c ← any @@ -84,6 +115,9 @@ ∨ ('a' ≤ c ∧ c ≤ 'f') ∨ ('A' ≤ c ∧ c ≤ 'F') then return c else fail s!"hex digit expected" +/-- +Parse an ASCII letter `a-z` or `A-Z` as a `Char`. +-/ @[inline] def asciiLetter : Parser Char := attempt do let c ← any @@ -99,14 +133,18 @@ else it +/-- +Skip whitespace: tabs, newlines, carriage returns, and spaces. +-/ @[inline] def ws : Parser Unit := fun it => .success (skipWs it) () + def take (n : Nat) : Parser String := fun it => let substr := it.extract (it.forward n) if substr.length != n then - .error it s!"expected: {n} codepoints" + .error it .eof else .success (it.forward n) substr