The Coq mailing list

[Bill Richter <richter AT math.northwestern.edu>]

I have an Ocaml question that the folks on the HOL and Ocaml newsgroups 
couldn't answer for me, and maybe it came up in writing Coq.  The basic 
Scheme exercise is to write a Scheme interpreter as a Scheme programmer.  I 
think that's called a meta-interpreter.  This isn't hard because of the 
Scheme quote feature, which allows you to turn your ``source'' program into a 
list that you then manipulate.  My question is: how do you this in Ocaml?  
How do you write an Ocaml meta-interpreter?  My interest is much more narrow. 
 I wrote an Ocaml program that functions to change the syntax of HOL Light 
http://code.google.com/p/hol-light/source/browse/trunk/RichterHilbertAxiomGeometry/README?spec=svn195&r=195
which is based on what I believe the Ocaml experts consider to be bad coding: 

(* From update_database.ml: Execute any OCaml expression given as a string.  
*)

let exec = ignore o Toploop.execute_phrase false Format.std_formatter
  o !Toploop.parse_toplevel_phrase o Lexing.from_string;;

I know the Ocaml experts think using Obj.magic is bad coding, but I get the 
impression they don't like Toploop either. 

My code thinks of a HOL Light program as a string and then uses exec to 
evaluate parts of the string.  Maybe the smart play is to understand camlp 
better and to write a parser that breaks down a HOL Light program as a list, 
much as the Scheme quote function does.  Does anyone know how to do this?  
Did this issue arise in writing Coq as an Ocaml program? 

-- 
Best,
Bill