[racket] proof assistants, DrRacket and Bootstrap

From: Bill Richter (richter at math.northwestern.edu)
Date: Sun Sep 28 00:57:12 EDT 2014

   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. 


Posted on the users mailing list.