[racket] proof assistants, DrRacket and Bootstrap

   Translating the gist of suggestions to such posters, I would say:
   do you really need to execute *any* expression? If not, use
   OCamllex and/or OCamlyacc (maybe Menhir, or a smaller and cleaner
   parser combinator library) to write a parser for your language
   subset, and then write an interpreter for the resulting ASTs.

Thanks, Prabhakar!  I think something like what you're saying is true.  HOL Light is based on quite a lot of the OCaml parser camlp, and I've thought for a long time that I had to learn it myself.  

   I don't have enough practice in OCaml to grasp what your code does

I'm making a dialect ofHOL Light with different syntax by interpreting one of my programs as a string and then breaking the string up into the component pieces, but then I need this Toploop/exec hack to evaluate my variables.  That sounds like the Scheme eval, and in Scheme you can solve that problem nicely with the quote feature. 

-- 
Best,
Bill