parser.lean

definition position := nat

inductive result (I : Type) : Type -> Type
| fail : Π {R}, I -> list string -> string -> result R
| partial : Π {R}, (I -> result R) -> result R
| done : Π {R}, I -> R -> result R

open result

definition result.map {A B I : Type} (f : A → B) : result I A -> result I B
| result.map (fail input contexts msg) := (fail input contexts msg)
| result.map (partial k) := partial (fun x, result.map (k x))
| result.map (done input res) := done input (f res)