diff --git a/theories/Parser.v b/theories/Parser.v index f00304d..536b02f 100644 --- a/theories/Parser.v +++ b/theories/Parser.v @@ -141,14 +141,18 @@ Arguments until {_ _ _}. Arguments untilMulti {_ _ _}. Definition parse' {T} (p: parser T) (acc: list ascii) (str: string) - : option string + T * list ascii := - match runStateT p (acc ++ list_ascii_of_string str)%list with - | inl e => inl e - | inr sl => inr sl + : (option string + T) * list ascii := + let input : list ascii := (acc ++ list_ascii_of_string str)%list in + match runStateT p input with + | inl e => (inl e, input) + | inr (s, l) => (inr s, l) end. -Definition parse {T} (p: parser T) (str: string) : option string + T * string := +Definition deprecated_parse {T} (p: parser T) (str: string) : option string + T * string := match parse' p [] str with - | inl e => inl e - | inr (s, l) => inr (s, string_of_list_ascii l) + | (inl e, _) => inl e + | (inr res, remainder) => inr (res, string_of_list_ascii remainder) end. + +#[deprecated(note="Use parse' instead")] +Notation parse := deprecated_parse.