The computational aspect of it is the same old parser monad, type Parser s a = [s] -> [(s, [a])], which takes a list of tokens [s] to a (possibly empty) list (here is where backtracking/nondeterminism comes into it) of parses paired with the rest of the text. It's a monad and also a monad plus.
On the specification end, we can put a precondition on the input string (for example, you might say the input length is <= some value, for ensuring termination of a recursive parser) and also a post condition comparing the input with the parsed value and the remaining output.
Definition Pre := list s -> Prop.
Definition Post (t : Set) := list s -> t -> list s -> Prop.
Program Definition Parser (pre : Pre) (t : Set) (post : Post t) : Set :=
forall i : { t : list s | pre t }, list ({ (x, r) : t * list s | post i x r }).
in Haskell we might define:
m >>= f = \i -> concatMap (uncurry f) (m i)
And in Coq, using Program we have roughly the same thing. Except that one has to apply a 'noncomputational_map' to fudge the proofs paired up with the list elements.
Program Definition Bind (a b : Set) P1 P2 Q1 Q2
(m : Parser P1 a Q1)
(f : (forall x : a, Parser (P2 x) b (Q2 x))) :
Parser (fun i => P1 i /\ forall x o, Q1 i x o -> P2 x o)
b
(fun i x' o' => exists x o, Q1 i x o /\ Q2 x o x' o') :=
fun i => @flat_map ({ (x, o) : a * list s | Q1 i x o }) _
(fun xo => match xo with (x,o) => noncomputational_map _ _ _ _ (f x o) end)
(m i).
Seeing as noncomputational map doesn't do anything, we prove a theorem expressing that as justification for extracting it out as the identity function (rather it being equivalent to map id traversing the whole list).
Theorem noncomputational_map_identity :
forall l,
map (@proj1_sig _ _) l = map (@proj1_sig _ _) (noncomputational_map l).
Extract Inlined Constant noncomputational_map => "id".
Another nice parser combinator is the fixed point of a parser:
Program Definition Fix t {P Q} :
(forall i : { t : list s | P t },
Parser (fun i' => length i' < length i /\ P i') t Q ->
list ({ (x, o) : t * list s | Q i x o })) ->
Parser P t Q :=
fun Rec =>
well_founded_induction
(well_founded_ltof ({ i : list s | P i }) (fun i => length i))
(fun i => list ({ (x, o) : t * list s | Q i x o }))
(fun x Rec' => Rec x (fun i => Rec' i _)).
It packages up well founded recursion on the size of the input string, so that any non-left recursive parsers should be easily defined.
Enough of the heavy machinary! A simple example of putting thing into work now:
<par> ::= <epsilon> | '(' <par> ')' <par>To parse this we define a type of tokens and abstract syntax of parsing derivations - then relate them with a function:
Inductive token := open | close.
Inductive par := epsilon : par | wrappend : par -> par -> par.
Fixpoint print (p : par) : list token :=
match p with
| epsilon => nil
| wrappend m n => (open::nil) ++ print m ++ (close::nil) ++ print n
end.
Now Program lets us define the par parser as the fixed point of the sum of epsilon and wrapped recursions:
Program Definition par_parser : Parser token (fun _ => True) par (fun x p y => x = print p ++ y /\ length y <= length x) :=
Fix token par (fun i parRec =>
Plus _ _ (fun i' => i = i') _
(fudge_pre_and_post_conditions _ _ _
(Return epsilon))
(fudge_pre_and_post_conditions _ _ _
(Symbol token eq_token_dec open >>= fun _ =>
parRec >>= fun m =>
Symbol token eq_token_dec close >>= fun _ =>
parRec >>= fun n =>
Return (wrappend m n)))
i).
Here are the actual scripts http://github.com/odge/parseq/tree/master
