I'm trying to write a program in Coq to parse a relatively simple context-free grammar (one type of parenthesis) and my general algorithm is for the parser to potentially return the remainder of a string. For example, parsing "++]>><<"
should return CBTerminated [Incr Incr] ">><<"
and then, say a parser that is parsing "[++]>><<" would be able to pick up the ">><<" and continue with that.
So obviously, the string is smaller, but convincing Coq of that is another matter. It is giving me the error
Recursive definition of parseHelper is ill-formed. [...] Recursive call to parseHelper has principal argument equal to "rest'" instead of "rest".
Which I assume means that it isn't convinced that rest' < input
in the way that it's convinced that rest < input
. (where <
means "is smaller than").
I'd thought of instead returning a count of how many characters to skip, but that seems rather inelegant and uneccessary.
Require Import Coq.Strings.String.
Require Import Coq.Strings.Ascii.
Require Import Coq.Lists.List.
Require Import ZArith.
Open Scope char_scope.
Open Scope list_scope.
Notation " [ ] " := nil (format "[ ]") : list_scope.
Notation " [ x ] " := (cons x nil) : list_scope.
Notation " [ x ; y ; .. ; z ] " := (cons x (cons y .. (cons z nil) ..)) : list_scope.
Inductive BF :=
| Incr : BF
| Decr : BF
| Left : BF
| Right : BF
| In : BF
| Out : BF
| Sequence : list BF -> BF
| While : BF -> BF.
Inductive BF_Parse_Result :=
| UnmatchedOpen
| EOFTerminated (u : list BF)
| CBTerminated (u : list BF) (rest : string).
Definition bind (val : BF) (onto : BF_Parse_Result) :=
match onto with
| UnmatchedOpen => UnmatchedOpen
| EOFTerminated values => EOFTerminated (cons val values)
| CBTerminated values rest => CBTerminated (cons val values) rest
end.
Fixpoint parseHelper (input : string) : BF_Parse_Result :=
match input with
| EmptyString => EOFTerminated nil
| String first rest =>
match first with
| "+" => bind Incr (parseHelper rest)
| "-" => bind Decr (parseHelper rest)
| "<" => bind Left (parseHelper rest)
| ">" => bind Right (parseHelper rest)
| "," => bind In (parseHelper rest)
| "." => bind Out (parseHelper rest)
| "]" => CBTerminated nil rest
| "[" =>
match parseHelper rest with
| UnmatchedOpen => UnmatchedOpen
| EOFTerminated _ => UnmatchedOpen
| CBTerminated vals rest' =>
bind (While (Sequence vals)) (parseHelper rest')
end
| _ => parseHelper rest
end
end.
Have you considered using well-founded recursion? Coq's standard library has a series of useful combinators for defining functions over well-founded relations. Reference 1 shows two techniques (well-founded recursion and a monad) for general recursion.
Other technique that is also very useful in context of Agda, is the so-called Bove-Capretta method, which defines an inductive predicate that mimics the call graph of defined function.
Coq also has the Function command that can be used to define more general recursive functions. Whenever I needed to define non-structurally recursive functions, I have used well-founded recursion.
Hope that this helps you.
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With