English version
Accueil     À propos     Téléchargement     Ressources     Contactez-nous    

Ce site est rarement mis à jour. Pour les informations les plus récentes, rendez-vous sur le nouveau site OCaml à l'adresse ocaml.org.

Browse thread
Incremental, undoable parsing in OCaml as the general parser inversion
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: 2007-07-05 (23:02)
From: oleg@p...
Subject: Re: [Caml-list] Incremental, undoable parsing in OCaml as the

The claim of *mechanical*, automatic and universal inversion of
existing, unmodified, separately compiled parsers, etc. stands.

I believe we have a mis-understanding. There are TWO implementations
of delimited continuations for OCaml. One is the monadic, implemented
in pure 100% OCaml and available for both bytecode and native
compilers. The other is non-monadic implementation, which is at
present available for byte-code only. Paul Snively asked we about the
first, monadic one. To use that implementation, one indeed has to
re-write the parser and everything else for that matter in monadic

The original message was talking about the non-monadic, direct style
approach. There, the inversion of the parser works automatically and
mechanically. There is no need to re-write the parser or anything

John Skaller wrote:
> What you've shown is that it is possible to *manually*
> control invert a given algorithm.
> Now you should note what Felix does. It *mechanically*
> control inverts any algorithm encoded with Felix procedures.
> And I mean *concrete syntax* here :)

The original message demonstrated how to *mechanically* and
automatically invert the given algorithm. You could have tried it
yourself: the runnable code was included. The code specifically used
Genlex.make_lexer from the standard library as it is. The code also
used Stream.iter, Stream.from and other library functions -- as they
are, as they *had* been compiled and placed in the standard
library. No modifications were done to any of these functions.

> But this isn't so, because you confuse the meaning of 'parser'
> and 'implementation' to a programmer, as compared to a
> theoretician. A programmer thinks an 'implementation' is
> concrete syntax .. i.e. an actual text file.. a theoretician's
> 'concrete syntax' is still an abstract encoding.

I assure you that I'm an industrial programmer and I don't confuse
concrete with abstract syntax. When the message said that the
procedure to invert a parser is mechanical and independent of the
parser implementation, it meant exactly that and for what _you_ call
`concrete syntax'. The message itself contained the proof: the
complete code. If you consider that evidence unsatisfactory, please
send me your parser (that can be compiled with OCaml 3.09) and I will
send you the proof of inversion without modifying a bit of your
code. You can run that code for yourself. You could just send me
compiled *.cmi and *cmo files instead (but I need to check the precise
version of my system then so it can load your files).

> This shows that monads have all the same problems as
> ordinary imperative code if you over use them
> (as of course is common practice in low level procedural
> programming languages).

Partly I agree with you. Still, with monad and an expressive type
system, one can do better (for example, assure that operations on
memory pointers respect alignment and sizes of memory area, even if we
permit pointer arithmetic). That was the subject of a recent paper on
strongly typed memory areas
We can even statically reason about some timing constraints.

Paul Snively wrote:
> what the issues in providing delimited continuations natively for
> ocamlopt are?

I guess the major issue is of not actually trying. I believe the
simple and inefficient version (which just copies the stack) can be
done relatively quickly. I need to check if there are any absolute
pointers in the stack to locations on the stack itself (but I don't
think they are). In any case, frame tables describe exactly what is on
the stack. A more efficient version is to make the stack segmented;
that takes longer.