Thanks, Prabhakar, this is exactly what I wanted, and you know something about
it (I was barely able to install Coq):
I am teaching a grad course using Coq right now, and using Proof
General within Emacs for it. That is not bad, but I would love to
have a DrRacket interface.
> OCaml doesn't have a quote feature, so the question arises how to
> write an OCaml interpreter inside OCaml.
In my senior undergraduate programming language course, I have them
write various interpreters and typecheckers in various languages,
including Racket, OCaml, and Haskell.
[...]
I know this is way off-topic, but it seems to me that Schemers are the only
people who want an elegant solution here:
But parsing an expression written in faux OCaml/Haskell is quite
complicated. [...] Parsing is much easier in Racket/Scheme because
of the similarity of code/data and the presence of 'read'.
I think it's a parsing question I'm stuck on. I think I need to use camlp to
avoid the following hack/kludge which I learned from the HOL Light experts,
found in my file
hol_light/RichterHilbertAxiomGeometry/readable.ml
which is part of the HOL Light distribution:
(* 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;;
(* Following miz3.ml, exec_thm returns the theorem representing a string, so *)
(* exec_thm "FORALL_PAIR_THM";; returns *)
(* val it : thm = |- !P. (!p. P p) <=> (!p1 p2. P (p1,p2)) *)
let thm_ref = ref TRUTH;;
let exec_thm s =
if Str.string_match (Str.regexp "[^;]*;") s 0 then raise Noparse
else
try exec ("thm_ref := (("^ s ^"): thm);;");
!thm_ref
with _ -> raise Noparse;;
When I posted my question on the OCaml list, the experts said don't ever use
Obj.magic, but I think they didn't think much of me using Toploop either.
--
Best,
Bill
____________________
Racket Users list:
http://lists.racket-lang.org/users
