[Caml-list] Obj.magic, Toploop, HOL Light & pretty-printing exceptions

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

I'm an HOL Light programmer, and I'd like to understand Obj.magic and Toploop, which aren't explained in the ocaml doc http://caml.inria.fr/pub/docs/manual-ocaml-4.00/index.html.  I think Obj.magic and Toploop should be well explained, as they seem similar to the Scheme quote feature which allows one to write a Scheme->Scheme meta-interpreter.  That's the sort of thing I'm trying to do in
hol_light/RichterHilbertAxiomGeometry/readable.ml
included in the latest HOL Light subversion (see http://www.cl.cam.ac.uk/~jrh13/hol-light), which crucially use `exec' from 
hol_light/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;;

   (* Evaluate any OCaml expression given as a string. *)

   let eval n =
     exec ("let buf__ = ( " ^ n ^ " );;");
     Obj.magic (Toploop.getvalue "buf__");;

BTW I got segfaults when I used `eval'.  I'd like to thank the expert HOL Light programmers who taught me, John Harrison, Freek Wiedijk (who wrote my model meta-interpreter hol_light/miz3/miz3.ml), Vince Aravantinos and Mark Adams, but I'd like to understand my own code better.  Mark explained everything I know about `exec', with:

   Roughly speaking it takes a string, turns it into lexical tokens,
   turns this into abstract syntax and then executes it.

The file hol_light/update_database.ml begins 

(* ========================================================================= *)
(* Create search database from OCaml / modify search database dynamically.   *)
(*                                                                           *)
(* This file assigns to "theorems", which is a list of name-theorem pairs.   *)
(* The core system already has such a database set up. Use this file if you  *)
(* want to update the database beyond the core, so you can search it.        *)
(*                                                                           *)
(* The trickery to get at the OCaml environment is due to Roland Zumkeller.  *)
(* It works by copying some internal data structures and casting into the    *)
(* copy using Obj.magic.                                                     *)
(* ========================================================================= *)

Here's another question about pretty-printing exception messages. 
This code from readable.ml, essentially due to Mark Adams, does a pretty good job printing my error messages:

   exception Readable_fail of string;;

   let printReadExn e =
     match e with
     | Readable_fail s
	  -> print_string s
     | _  -> print_string (Printexc.to_string e);;

   #install_printer printReadExn;;

But I know that with other exceptions, the behavior isn't quite identical to normal exception printing, as I would have preferred.

A last question: I'm not sure I understood the indentation rules for multiple if/then/else explained in 
http://caml.inria.fr/resources/doc/guides/guidelines.en.html
Maybe someone can look at the 97 lines of code in my readable.ml beginning with
let rec StringToTactic s =

-- 
Best,
Bill