Imports
Our Parser relation works as highlevel specification, it is just a relation that evaluates to True or False according their inputs, but once we move into the area of implementation we need to return more complex types, and take error handling into account. That's the purpose of ParseError
inductive ParseError where
| unexpectedToken (expected : String) (found : String)
| unexpectedEnd (expected : String)
| expectingOneOf (choice₀ choice₁ : ParseError)
| alwaysFails
| guardFailed
| noProgress
deriving DecidableEq, ReprRdParser stands for Recursive Descent Parser and for each one of it there is a corresponding Parser specification.
abbrev RdParser α := List String → Except ParseError (α × List String)
tk corresponds to Parsing.tk
def tk (s: String) : RdParser String :=
fun xs =>
match xs with
| [] => .error (.unexpectedEnd s)
| y :: ys =>
if y = s
then .ok (y, ys)
else .error (.unexpectedToken s y)
any corresponds to Parsing.any
def any : RdParser String :=
fun input =>
match input with
| [] => .error (.unexpectedEnd "")
| x :: xs => .ok (x, xs)
pure corresponds to Parsing.pure
def pure (x: α): RdParser α :=
fun input => .ok (x, input)
fail corresponds to Parsing.fail
def fail : RdParser α :=
fun _input => .error .alwaysFails
choice corresponds to Parsing.first_choice: it tries the first parser,
and if it fails then it tries the second one.
def choice (p q: RdParser α): RdParser α :=
fun input =>
match p input with
| .ok (r, rest) => .ok (r,rest)
| .error e =>
match q input with
| .ok (r, rest) => .ok (r, rest)
| .error f =>
.error (.expectingOneOf e f)FollowsSpec defines the correspondence between parser implementation and specification: an implementation follows a specification when it succeeds exactly on the inputs, results, and remaining tokens that the specification relates.
def FollowsSpec (impl: RdParser α) (spec: Syntax.Parsing.Parser α) : Prop :=
∀ input result rest,
impl input = .ok (result, rest) ↔ spec input result rest
seq corresponds to Parsing.seq
def seq (p: RdParser α) (q: RdParser β): RdParser (α × β) :=
fun input =>
match p input with
| .ok (rp, rest_p) =>
match q rest_p with
| .ok (rq, rest_q) => .ok ((rp, rq), rest_q)
| .error eq => .error eq
| .error eq => .error eq
many corresponds to Parsing.many: it keeps applying its parser until
it fails, and fails itself when an application succeeds without
consuming any input.
def many (p: RdParser α): RdParser (List α) :=
fun input =>
match p input with
| .ok (x, first_rest) =>
if first_rest.length < input.length then
match many p first_rest with
| .ok (xs, rem_rest) => .ok (x :: xs, rem_rest)
| .error e => .error e
else
.error .noProgress
| .error _ => .ok ([], input)
termination_by input => input.length
map corresponds to Parsing.map
def map (f: α → β) (p: RdParser α): RdParser β :=
fun input =>
match p input with
| .ok (x, rest) => .ok (f x, rest)
| .error e => .error e
guardp corresponds to Parsing.guardp
def guardp (f: α → Bool) (p: RdParser α): RdParser α :=
fun input =>
match p input with
| .ok (x, rest) =>
if f x then .ok (x, rest) else .error .guardFailed
| .error e => .error e
all_digits and all_alpha reuse Parsing.all_digits and
Parsing.all_alpha as predicates on tokens.
def all_digits := Syntax.Parsing.all_digitsdef all_alpha := Syntax.Parsing.all_alpha
digits and alpha correspond to Parsing.digits and Parsing.alpha
def digits := guardp all_digits any
left corresponds to Parsing.left
right corresponds to Parsing.right