Parser specifications — Programming Language Theories

Parser

Parser defines the signature of a relation between an input tokens, a result value, and the remaining tokens after parsing that value. Those relations are not meant to implement parsing, just to declare the behavior of parsers to then prove the correctness of any implementation.

abbrev Parser (α: Type) := List String → α → List String → Prop

tk illustrates the above introduction: given a token, specifies the behavior of a parser that recognizes that token at the head of input, or fails.

@[reducible]
def tk (s: String): Parser String :=
  fun input result rest =>
    input = s :: rest ∧ result = s

any specifies the behavior of a parser that always succeeds on non-empty sequences of tokens, consuming the head token.

@[reducible]
def any : Parser String :=
  fun input result rest => input = result :: rest

pure consumes no input and returns its parameter as successfully parsed result

@[reducible]
def pure (x: α) : Parser α :=
  fun input result rest => result = x ∧ rest = input

fail always fails to parse.

@[reducible]
def fail : Parser α := fun _input _result _rest => False

choice succeeds if any of the parsers passed as argument succeeds, in no particular order, i.e. non-deterministically.

@[reducible]
def choice (x y : Parser α) : Parser α :=
  fun input result rest =>
    x input result rest ∨ y input result rest

first_choice is a more convenient specification for the choice like behavior described above, since implementations tend to deterministically try the first parser, and if it fails then they try the second. To rely on the above choice definition would make proofs to cumbersome for some typical implementations.

@[reducible]
def first_choice (x y : Parser α) : Parser α :=
  fun input result rest =>
    x input result rest ∨
      ((¬ ∃ r s, x input r s) ∧ y input result rest)

instance : OrElse (Parser α) where
  orElse p q := choice p (q ())

seq applies two parsers sequentially. The first on the original input, the second on the remaining tokens after the first succeeds. Both results are compound the resulting tuple value.

@[reducible]
def seq (p: Parser α) (q: Parser β): Parser (α × β) :=
  fun input result rest =>
    ∃ a b mid, result = (a, b) ∧ p input a mid ∧ q mid b rest

infixl:60 " <*> " => seq

many applies a parser zero or more times, resulting on a list of values.

@[reducible]
def many (p: Parser α): Parser (List α)
  | input, [], rest => input = rest
  | input, a :: results, rest =>
    ∃ mid, p input a mid ∧ many p mid results rest

map applies a function to the result value of a successful Parser

@[reducible]
def map (f: α → β) (p: Parser α): Parser β :=
  fun input result rest =>
    ∃ a, p input a rest ∧ f a = result

infixr:100 " <$> " => map

guardp constraints the success of a parser using a predicate f on its result value

@[reducible]
def guardp(f: α → Bool) (p: Parser α): Parser α :=
  fun input result rest =>
    (f result) ∧ p input result rest

def all_digits (xs: String) := xs.all Char.isDigitdef all_alpha (xs: String) := xs.all Char.isAlpha

digits and alpha are convenient specifications for parsers that succeed only on digit tokens and alphabetic characters respectively.

def digits := guardp all_digits any

def alpha := guardp all_alpha any

left applies two parsers but only returns the result of the first one

@[reducible]
def left (p: Parser α) (q: Parser β): Parser α :=
  fun input result rest =>
    ∃ mid ignored, p input result mid ∧ q mid ignored rest

infixl:60 " <* " => left

right applies two parsers but only returns the result of the second one

@[reducible]
def right (p: Parser α) (q: Parser β): Parser β :=
  fun input result rest =>
    ∃ mid ignored, p input ignored mid ∧ q mid result rest

infixl:60 " *> " => right