Version française
Home     About     Download     Resources     Contact us    
Browse thread
camlp4 rewrites
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: -- (:)
From: David Monniaux <David.Monniaux@e...>
Subject: camlp4 rewrites
I'm currently playing with Coq and extraction, and I'm having the 
following problems:
* Since the list constructor of standard OCaml (infix ::) is not (yet) 
usable as a prefix ( :: ), I cannot just tell Coq to extract lists to 
OCaml lists. (Future OCaml versions will allow prefix ( :: ), I'm told.)
* OCaml compiles match e with true -> x1 | false -> x2 less efficiently 
than if e then x1 else x2 (bug report filed, but not fixed so far).

Unless I'm greatly mistaken, this can be fixed by a mere syntactic 
transformation using Camlp4. I suppose I'm not the first person to have 
encountered these problems... So has anybody done the necessary Camlp4 
scripts? :-)