On 12/11/2011 2:35 PM, Gabriel Scherer wrote:
I wonder how much energy it would take to create a stand-alone extensible parser library, implemented in pure OCaml (normal syntax), and following a similar API and semantics as camlp{4,5}, on which Coq parsing could be built.You are suggesting a dynamic parser tool. This is already available as the dypgen tool: http://dypgen.free.fr/ I suspect adapting Coq to such a tool would require considerable work, because the devil is in the details and they really need backward compatibility. I'm already impressed they managed to support both camlp4 and camlp5.
Agreed. It would probably be a lot easier to adapt Coq to work with a (new) parsing library that uses the same parsing algorithms as Camlp4.
-- Alain -- Caml-list mailing list. Subscription management and archives: https://sympa-roc.inria.fr/wws/info/caml-list Beginner's list: http://groups.yahoo.com/group/ocaml_beginners Bug reports: http://caml.inria.fr/bin/caml-bugs
